ext — Mathlib

English

Two DivInvMonoid structures are equal if both multiplication and inverse operations agree.

Русский

Две DivInvMonoid структуры равны, если совпадают их умножение и обратная операция.

LaTeX

$$$m_1 = m_2 \text{ if } (\forall x,y, x *_{m_1} y = x *_{m_2} y) \text{ and } (Inv_{m_1}(x) = Inv_{m_2}(x)\,\forall x)$$$

Lean4

@[to_additive (attr := ext)]
theorem ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄
    (h_mul :
      (letI := m₁;
          HMul.hMul :
          M → M → M) =
        (letI := m₂;
          HMul.hMul :
          M → M → M))
    (h_inv :
      (letI := m₁;
          Inv.inv :
          M → M) =
        (letI := m₂;
          Inv.inv :
          M → M)) :
    m₁ = m₂ := by
  have h_mon := Monoid.ext h_mul
  have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon
  let f : @MonoidHom M M m₁.toMulOne m₂.toMulOne :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁) (fun x y => congr_fun (congr_fun h_mul x) y)
  have : m₁.zpow = m₂.zpow := by
    ext m x
    exact @MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m
  have : m₁.div = m₂.div := by
    ext a b
    exact @map_div' _ _ (F := @MonoidHom _ _ (_) _) _ (id _) _ inferInstance f (congr_fun h_inv) a b
  rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩⟩
  congr

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