Commit 2025-09-23 16:16 238545e6

View on Github →

chore: remove redundant haveI/letI (#29908) These haveI and letI invocations seem to be remnants of lean3, when local variables weren't automatically added as instances.

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Set/Finite.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

Modified Mathlib/Probability/Kernel/WithDensity.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean