Theorems · Definition · commutative algebra

normalize

{α : Type u_1} → [inst : MonoidWithZero α] → [NormalizationMonoid α] → α → α

Chooses an element of each associate class, by multiplying by normUnit

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

137 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 41 definitions · uses no axioms

Assumes

MonoidWithZeroNormalizationMonoid