toAddMonoidHom_commutes — Mathlib

English

The additive-equivalence underlying a linear equivalence equals the linear equivalence itself.

Русский

Аддитивная эквивалентность, лежащая в основе линейной эквивалентности, равна самой линейной эквивалентности.

LaTeX

$$$\\mathrm{coe\\_toAddEquiv}(e) = e$$$

Lean4

/-- The two paths coercion can take to an `AddMonoidHom` are equivalent -/
theorem toAddMonoidHom_commutes : e.toLinearMap.toAddMonoidHom = e.toAddEquiv.toAddMonoidHom :=
  rfl

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