Theorem DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem

Modification history

2026-09-29 11:08
Mathlib/RingTheory/DividedPowers/RatAlgebra.lean
chore: rename remaining `not_mem` declarations to `notMem` (#44296) …
Deleted DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_memView on Github →
2025-09-05 17:21
Mathlib/RingTheory/DividedPowers/RatAlgebra.lean
feat(RingTheory/DividedPowers/RatAlgebra): add definitions (#22322) …
Added DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_memView on Github →