Theorem add_pow_eq_add_pow_mod_mul_pow_add_pow_div

Modification history

2024-10-21 22:54
Mathlib/Algebra/CharP/Basic.lean
refactor: merge `ExpChar` and `CharP` API (#18023) …
Deleted add_pow_eq_add_pow_mod_mul_pow_add_pow_divView on Github →
2024-07-23 14:14
Mathlib/Algebra/CharP/Basic.lean
feat(Data/Nat/Choose): Lucas' theorem (#8612) …
Added add_pow_eq_add_pow_mod_mul_pow_add_pow_divView on Github →