Theorem abs_pow_sub_pow_le

Modification history

2025-01-04 14:04
Mathlib/Algebra/Order/Ring/Abs.lean
chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242) …
Added abs_pow_sub_pow_leView on Github →