Commit 2025-03-29 00:46 acebdecb

View on Github →

chore: use induction tactic with Set.Finite.induction_on (#23415) This seems rather more readable.

Estimated changes

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/Data/Set/Finite/Lattice.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/Order/Filter/Finite.lean

Modified Mathlib/Order/Filter/Ultrafilter/Basic.lean

modified theorem Ultrafilter.finite_sUnion_mem_iff

Modified Mathlib/RingTheory/Finiteness/Nakayama.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

Modified Mathlib/Topology/Basic.lean

modified theorem Set.Finite.isOpen_sInter

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean