subtype_isoBaseOfIsPrincipal_eq_mul

English

Same structural equality as above, describing the interaction of subtype and isoBaseOfIsPrincipal with multiplication.

Русский

Та же структурная равенство, описывающее взаимодействие подпорядка и isoBaseOfIsPrincipal в умножении.

LaTeX

$$$(Submodule.subtype I) \circ (Ideal.isoBaseOfIsPrincipal h) = \mathrm{LinearMap.mul}(R,R,\mathrm{IsPrincipal.generator } I)$$$

Lean4

theorem subtype_isoBaseOfIsPrincipal_eq_mul {I : Ideal R} [hprinc : I.IsPrincipal] (h : I ≠ ⊥) :
    Submodule.subtype I ∘ₗ ↑(Ideal.isoBaseOfIsPrincipal h) = LinearMap.mul R R (IsPrincipal.generator I) :=
  by
  ext
  simp

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