ext — Mathlib

English

Two MulChar χ, χ′ are equal if they agree on all units of R.

Русский

Два MulChar χ, χ′ равны, если они совпадают на всех единицах R.

LaTeX

$$$\forall a\in R^×:\ χ(a)=χ'(a) \Rightarrow χ=χ'.$$$

Lean4

/-- Extensionality. Since `MulChar`s always take the value zero on non-units, it is sufficient
to compare the values on units. -/
@[ext]
theorem ext {χ χ' : MulChar R R'} (h : ∀ a : Rˣ, χ a = χ' a) : χ = χ' :=
  by
  apply ext'
  intro a
  by_cases ha : IsUnit a
  · exact h ha.unit
  · rw [map_nonunit χ ha, map_nonunit χ' ha]

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