Theorems · Definition · commutative algebra

Associates.out

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

Maps an element of Associates back to the normalized element of its associate class

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

15 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidWithZeroNormalizationMonoid