Commit 2026-01-28 08:39 49acf8f8

View on Github →

feat(Algebra/Order): injectivity of zpow in its left argument (#23177)

Estimated changes

added theorem zpow_left_injOn₀
added theorem zpow_left_inj₀
added theorem MySet.empty_union
deleted theorem Set.empty_union