Commit 2026-10-29 14:31 c9ca884d

View on Github →

feat: use IsApply for AddChar (#45338)

Estimated changes

Modified Mathlib/Algebra/Group/AddChar.lean

deleted theorem AddChar.add_apply

modified theorem AddChar.coe_eq_one

modified theorem AddChar.coe_mul

modified theorem AddChar.coe_one

modified theorem AddChar.coe_pow

deleted theorem AddChar.mul_apply

deleted theorem AddChar.nsmul_apply

deleted theorem AddChar.one_apply

deleted theorem AddChar.pow_apply

deleted theorem AddChar.prod_apply

deleted theorem AddChar.sum_apply

deleted theorem AddChar.zero_apply

Modified Mathlib/Analysis/Complex/Circle.lean

Modified Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/Galois/Infinite.lean

Modified Mathlib/GroupTheory/FiniteAbelian/Duality.lean

Modified Mathlib/LinearAlgebra/Transvection/Generation.lean

Modified Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean