Theorem sub_pow_eq_sub_pow_mod_mul_pow_sub_pow_div

Modification history

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