groupWithZeroOfCancel — Mathlib

English

Every finite nontrivial cancellative monoid with zero can be extended to a group with zero.

Русский

Каждое конечное ненулевое отменяющее мономиод с нулём можно расширить до группы с нулём.

LaTeX

$$def groupWithZeroOfCancel (M) [CancelMonoidWithZero M] [DecidableEq M] [Fintype M] [Nontrivial M] : GroupWithZero M$$

Lean4

/-- Every finite nontrivial cancel_monoid_with_zero is a group_with_zero. -/
def groupWithZeroOfCancel (M : Type*) [CancelMonoidWithZero M] [DecidableEq M] [Fintype M] [Nontrivial M] :
    GroupWithZero M :=
  { ‹Nontrivial M›,
    ‹CancelMonoidWithZero
        M› with
    inv := fun a => if h : a = 0 then 0 else Fintype.bijInv (mul_right_bijective_of_finite₀ h) 1
    mul_inv_cancel := fun a ha => by
      simp only [dif_neg ha]
      exact Fintype.rightInverse_bijInv _ _
    inv_zero := by simp }

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