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 x✝ : A
⊢ x✝ ∈ comap (↑(opLinearEquiv R)) 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
⊢ comap (↑(opLinearEquiv R)) 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 x✝ : A
⊢ x✝ ∈ comap (↑(opLinearEquiv R)) 1 ↔ x✝ ∈ 1
simp