toEuclideanDomain — Mathlib

English

Every field K carries a Euclidean-domain structure with division by b giving quotient a/b and remainder a − a·b/b; in particular, division with remainder exists for all a,b≠0.

Русский

Каждое поле K обладает структурой евклидова кольца: для любых a,b с b≠0 существует деление a = q·b + r с остатком r, причем остаток r равен 0 при dívida.

LaTeX

$$$\\mathrm{EuclideanDomain}(K)$$$

Lean4

instance (priority := 100) toEuclideanDomain : EuclideanDomain K :=
  { toCommRing := toCommRing
    quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
    quotient_mul_add_remainder_eq := fun a b => by by_cases h : b = 0 <;> simp [h, mul_div_cancel₀]
    r := fun a b => a = 0 ∧ b ≠ 0,
    r_wellFounded :=
      WellFounded.intro fun _ => (Acc.intro _) fun _ ⟨hb, _⟩ => (Acc.intro _) fun _ ⟨_, hnb⟩ => False.elim <| hnb hb,
    remainder_lt := fun a b hnb => by simp [hnb],
    mul_left_not_lt := fun _ _ hnb ⟨hab, hna⟩ => Or.casesOn (mul_eq_zero.1 hab) hna hnb }

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