ext — Mathlib

English

Let R be a type and A,B two NonAssocSemiring R-structures. If A and B have the same addition and the same multiplication, then A = B.

Русский

Пусть R — тип, A и B — структуры NonAssocSemiring R. Если операции сложения и умножения совпадают, то A = B.

LaTeX

$$$\\\\forall R \\, \\, \\forall A,B \in \\text{NonAssocSemiring}(R), \\\\ (+)_A = (+)_B \\\\land (*)_A = (*)_B \\\\Rightarrow A = B.$$$

Lean4

@[ext]
theorem ext ⦃inst₁ inst₂ : NonAssocSemiring R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ :=
  by
  have h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring := by ext : 1 <;> assumption
  have h_zero : (inst₁.toMulZeroClass).toZero.zero = (inst₂.toMulZeroClass).toZero.zero :=
    congrArg (fun inst => (inst.toMulZeroClass).toZero.zero) h
  have h_one' : (inst₁.toMulZeroOneClass).toMulOneClass.toOne = (inst₂.toMulZeroOneClass).toMulOneClass.toOne := by
    congr 2; ext : 1; exact h_mul
  have h_one : (inst₁.toMulZeroOneClass).toMulOneClass.toOne.one = (inst₂.toMulZeroOneClass).toMulOneClass.toOne.one :=
    congrArg (@One.one R) h_one'
  have : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne := by ext : 1 <;> assumption
  have : inst₁.toNatCast = inst₂.toNatCast := congrArg (·.toNatCast) this
  cases inst₁; cases inst₂
  congr

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