R : Type u_2
R₁ : Type ?u.396898
R₂ : Type ?u.396901
R₃ : Type ?u.396904
R₄ : Type ?u.396907
S : Type ?u.396910
K : Type ?u.396913
K₂ : Type ?u.396916
M : Type u_1
M' : Type ?u.396922
M₁ : Type ?u.396925
M₂ : Type ?u.396928
M₃ : Type ?u.396931
M₄ : Type ?u.396934
N : Type ?u.396937
N₂ : Type ?u.396940
ι : Type ?u.396943
V : Type ?u.396946
V₂ : Type ?u.396949
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
⊢ ⊥.toAddSubmonoid = ⊤.toAddSubmonoid ↔ ⊥ = ⊤
R : Type u_2
R₁ : Type ?u.396898
R₂ : Type ?u.396901
R₃ : Type ?u.396904
R₄ : Type ?u.396907
S : Type ?u.396910
K : Type ?u.396913
K₂ : Type ?u.396916
M : Type u_1
M' : Type ?u.396922
M₁ : Type ?u.396925
M₂ : Type ?u.396928
M₃ : Type ?u.396931
M₄ : Type ?u.396934
N : Type ?u.396937
N₂ : Type ?u.396940
ι : Type ?u.396943
V : Type ?u.396946
V₂ : Type ?u.396949
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
⊢ Subsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M)
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_eq]
no goals
R : Type u_2
R₁ : Type ?u.396898
R₂ : Type ?u.396901
R₃ : Type ?u.396904
R₄ : Type ?u.396907
S : Type ?u.396910
K : Type ?u.396913
K₂ : Type ?u.396916
M : Type u_1
M' : Type ?u.396922
M₁ : Type ?u.396925
M₂ : Type ?u.396928
M₃ : Type ?u.396931
M₄ : Type ?u.396934
N : Type ?u.396937
N₂ : Type ?u.396940
ι : Type ?u.396943
V : Type ?u.396946
V₂ : Type ?u.396949
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
⊢ ⊥.toAddSubmonoid = ⊤.toAddSubmonoid ↔ ⊥ = ⊤
rfl