Theorem one_lt_pow'

Modification history

2025-01-08 23:18

Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

feat: `a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n` (#20577) …

Modified one_lt_pow'View on Github →

2024-09-24 07:14

Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

chore(Monoid/Unbundled/Pow): cleanup (#17013)

Modified one_lt_pow'View on Github →

2023-10-30 16:19

Mathlib/Algebra/GroupPower/CovariantClass.lean

chore: split GroupPower/Order (#7978)

Modified one_lt_pow'View on Github →

2022-12-15 21:58

Mathlib/Algebra/GroupPower/Order.lean

feat: port Algebra.GroupPower.Order (#1043) …

Added one_lt_pow'View on Github →