intSpanEquivQuotAddOrderOf_apply_self

English

Applied to a, the isomorphism intSpanEquivQuotAddOrderOf a sends ⟨a, mem_span_singleton_self a⟩ to the class of 1 in the quotient.

Русский

Применяя изоморфизм intSpanEquivQuotAddOrderOf к ⟨a, mem_span_singleton_self a⟩, получаем класс 1 в фактор-модуле.

LaTeX

$$$\text{intSpanEquivQuotAddOrderOf } a (\langle a, \mathrm{Submodule.mem\_span\_singleton\_self}~a \rangle) = \mathrm{Submodule.Quotient}.mk 1$$$

Lean4

theorem intSpanEquivQuotAddOrderOf_apply_self (a : A) :
    intSpanEquivQuotAddOrderOf a ⟨a, Submodule.mem_span_singleton_self a⟩ = Submodule.Quotient.mk 1 :=
  (LinearEquiv.eq_symm_apply _).mp <| Subtype.ext (one_zsmul _).symm

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