Commit 2023-03-23 16:07 4a6b502d

View on Github →

chore: fix docs, golf, rename (#3010)

Run fix-comments on Mathlib/LinearAlgebra/Basis.lean.
Rename Basis.of_repr to Basis.ofRepr.
Reflow/minor golf.

Estimated changes

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/LinearAlgebra/Basis.lean

added theorem Basis.coe_ofRepr

deleted theorem Basis.coe_of_repr

modified def Basis.constr

added theorem Basis.eq_ofRepr_eq_repr

deleted theorem Basis.eq_of_repr_eq_repr

modified theorem Module.card_fintype

Modified Mathlib/LinearAlgebra/Dfinsupp.lean

Modified Mathlib/RingTheory/AlgebraTower.lean