R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
this : AlgHom.range (ofId R A) = ⊥
⊢ x ∈ Set.range ↑(ofId R A) ↔ x ∈ Set.range ↑(algebraMap R A)
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
this : AlgHom.range (ofId R A) = ⊥
⊢ x ∈ ⊥ ↔ x ∈ Set.range ↑(algebraMap R A)
rw [← this, ← SetLike.mem_coe, AlgHom.coe_range]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
this : AlgHom.range (ofId R A) = ⊥
⊢ x ∈ Set.range ↑(ofId R A) ↔ x ∈ Set.range ↑(algebraMap R A)
rfl