Theorem Irreducible.squarefree

Modification history

2026-10-07 11:06

Mathlib/Algebra/Squarefree/Basic.lean

feat(RingTheory): multiplicity at an irreducible element (#40301) …

Modified Irreducible.squarefree View on Github →

2023-03-21 21:27

Mathlib/Algebra/Squarefree.lean

feat: port Algebra.Squarefree (#3018)

Added Irreducible.squarefree View on Github →