Commit 2024-02-05 11:04 3284c6f2

View on Github →

chore(LinearAlgebra/Dual): Fintype -> Finite (#10265) Also use lowercase for DualBases axioms.

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

modified theorem BilinForm.dualSubmodule_dualSubmodule_flip_of_basis

modified theorem BilinForm.dualSubmodule_flip_dualSubmodule_of_basis

modified theorem BilinForm.dualSubmodule_span_of_basis

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem Basis.dualBasis_equivFun

modified theorem Basis.toDual_eq_equivFun

modified theorem Module.DualBases.coe_dualBasis