Theorem DividedPowers.OfSquareZero.dpow_of_two_le

Modification history

2025-09-05 17:21

Mathlib/RingTheory/DividedPowers/RatAlgebra.lean

feat(RingTheory/DividedPowers/RatAlgebra): add definitions (#22322) …

Added DividedPowers.OfSquareZero.dpow_of_two_le View on Github →