Commit 2024-02-05 09:20 fbee97e1

View on Github →

chore(Topology): Fintype -> Finite (#10262)

Estimated changes

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

modified theorem Basis.constrL_apply

modified theorem continuous_equivFun_basis

Modified Mathlib/Topology/Bases.lean

modified theorem TopologicalSpace.isSeparable_pi

Modified Mathlib/Topology/Bornology/Constructions.lean