Theorem add_pow_prime_pow_eq

Modification history

2025-11-04 13:39
Mathlib/Algebra/CharP/Lemmas.lean
refactor(Algebra/CharP): strengthen expansion of `(x + y) ^ p ^ n` (#31193) …
Modified add_pow_prime_pow_eqView on Github →
2024-10-24 20:59
Mathlib/Algebra/CharP/Basic.lean
chore(Algebra/CharP): reduce theory requirements for `CharP.Defs` (#18182) …
Modified add_pow_prime_pow_eqView on Github →
2024-10-14 10:52
Mathlib/Algebra/CharP/Basic.lean
refactor(CharP): make variables explicit + refactor (#14416) …
Modified add_pow_prime_pow_eqView on Github →
2023-04-01 16:09
Mathlib/Algebra/CharP/Basic.lean
chore: re-port Algebra.CharP.Basic (#3191) …
Added add_pow_prime_pow_eqView on Github →