instNontrivialUnits

Mathlib.Algebra.GroupWithZero.WithZero

URI: https://scilib.ai/kg/mathlib#WithZero.instNontrivialUnits

English

For γ ∈ (WithZero α)ˣ, the equation ↑(unitsWithZeroEquiv γ) = γ.val holds.

Русский

Для γ ∈ (WithZero α)ˣ выполняется ↑(unitsWithZeroEquiv γ) = γ.val.

LaTeX

$$$ \\uparrow( unitsWithZeroEquiv\\, \\gamma ) = \\gamma.\\mathrm{val} $$$

Lean4

instance [Nontrivial α] : Nontrivial (WithZero α)ˣ :=
  unitsWithZeroEquiv.toEquiv.surjective.nontrivial

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru