quotient — Mathlib

English

For any irreducible ϖ, addVal(ϖ) = 1.

Русский

Для любого ирредуцируемого ϖ, addVal(ϖ) = 1.

LaTeX

$$$\mathrm{addVal}(\varpi) = 1$$$

Lean4

/-- A noncomputable quotient to define the Euclidean domain structure. The GCD algorithm only takes
two steps to terminate. Given `GCD(x,y)`, if `x ∣ y` then `y%x = 0` so we're done in one step;
otherwise `y%x = y` and then `GCD(x,y) = GCD(y,x)` which brings us back to the first case. -/
def quotient (x y : R) : R :=
  open Classical in if y = 0 then 0 else if h : y ∣ x then h.choose else 0

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