case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
x✝ : A'
⊢ x✝ ∈ map (AlgHom.toLinearMap f) 1 ↔ x✝ ∈ 1
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map (AlgHom.toLinearMap f) 1 = 1
ext
no goals
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
x✝ : A'
⊢ x✝ ∈ map (AlgHom.toLinearMap f) 1 ↔ x✝ ∈ 1
simp