Commit 2025-06-27 00:26 f2ef672c

View on Github →

chore: golf using constructor (#26433)

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/Field/ZMod.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

modified theorem Polynomial.eta

Modified Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean

Modified Mathlib/CategoryTheory/Limits/Types/Shapes.lean

Modified Mathlib/Data/Bool/Basic.lean

modified theorem Bool.bne_eq_xor

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/FieldTheory/Galois/Infinite.lean

Modified Mathlib/RingTheory/MatrixPolynomialAlgebra.lean