isIdempotentElem_toSubmodule — Mathlib

English

For any Subalgebra S, the underlying submodule S.toSubmodule is idempotent under multiplication: S.toSubmodule · S.toSubmodule = S.toSubmodule.

Русский

Для любой подалгебры S соответствующий подмодуль S.toSubmodule удовлетворяет $S^{2}=S$ в смысле умножения подмодулей.

LaTeX

$$IsIdempotentElem(toSubmodule(S))$$

Lean4

/-- As submodules, subalgebras are idempotent. -/
@[simp]
theorem isIdempotentElem_toSubmodule (S : Subalgebra R A) : IsIdempotentElem S.toSubmodule :=
  by
  apply le_antisymm
  · refine (mul_toSubmodule_le _ _).trans_eq ?_
    rw [sup_idem]
  · intro x hx1
    rw [← mul_one x]
    exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

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