Theorem CharTwo.sum_sq

Modification history

2024-05-27 08:32

Mathlib/Algebra/CharP/Two.lean

chore: Use the new `∑ i ∈ s, f i` notation (#13209) …

Modified CharTwo.sum_sq View on Github →

2023-03-14 13:55

Mathlib/Algebra/CharP/Two.lean

feat: port Algebra.CharP.Two (#2873)

Added CharTwo.sum_sq View on Github →