Theorem UniqueFactorizationMonoid.of_existsUnique_irreducible_factors

Modification history

2026-01-20 16:34

Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

chore(Algebra): deprecate `CancelMonoidWithZero` (#33851) …

Modified UniqueFactorizationMonoid.of_existsUnique_irreducible_factors View on Github →

2024-12-18 19:47

Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

chore(Logic/ExistsUnique): amend usages of existsUnique to follow naming convention (#20028) …

Added UniqueFactorizationMonoid.of_existsUnique_irreducible_factors View on Github →