Theorem DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_lt

Modification history

2025-09-05 17:21
Mathlib/RingTheory/DividedPowers/RatAlgebra.lean
feat(RingTheory/DividedPowers/RatAlgebra): add definitions (#22322) …
Added DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_ltView on Github →