eq_bot_of_equiv — Mathlib

English

If a submodule is mapped by an equivalence to the bottom, it must be bottom.

Русский

Если подмодуль отображается эквивелентностью в нулевой подмодуль, то он сам нулевой.

LaTeX

$$theorem eq_bot_of_equiv (e : p ≃ₛₗ[σ₁₂] (⊥ : Submodule R₂ M₂)) : p = ⊥$$

Lean4

theorem eq_bot_of_equiv [Module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] (⊥ : Submodule R₂ M₂)) : p = ⊥ :=
  by
  refine bot_unique (SetLike.le_def.2 fun b hb => (Submodule.mem_bot R).2 ?_)
  rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff]
  apply Submodule.eq_zero_of_bot_submodule

Похожие утверждения