commGroupWithZero — Mathlib

English

ValueGroup(A,K) carries the structure of a commutative group with zero.

Русский

ValueGroup(A,K) обладает структурой коммутативной группы с нулём.

LaTeX

$$$\mathrm{ValueGroup}(A,K) \in \mathrm{CommGroupWithZero}$$$

Lean4

instance commGroupWithZero : CommGroupWithZero (ValueGroup A K) :=
  { mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]
    one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]
    mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]
    mul_comm := by rintro ⟨a⟩ ⟨b⟩; apply Quotient.sound'; rw [mul_comm]
    zero_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]
    mul_zero := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_zero]
    inv_zero := by apply Quotient.sound'; rw [inv_zero]
    mul_inv_cancel := by
      rintro ⟨a⟩ ha
      apply Quotient.sound'
      use 1
      simp only [one_smul]
      apply (mul_inv_cancel₀ _).symm
      contrapose ha
      simp only [Classical.not_not] at ha ⊢
      rw [ha]
      rfl }

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