Commit 2024-02-04 23:05 78c16c2f

View on Github →

feat(LinearAlgebra/Basis): assume [Finite ι] instead of [Fintype ι] (#10251)

Estimated changes

modified theorem Basis.coe_ofEquivFun
modified theorem Basis.constr_apply_fintype
modified theorem Basis.coord_equivFun_symm
modified def Basis.equivFun
modified theorem Basis.equivFun_apply
modified theorem Basis.equivFun_ofEquivFun
modified theorem Basis.equivFun_self
modified theorem Basis.equivFun_symm_apply
modified theorem Basis.map_equivFun
modified theorem Basis.mem_submodule_iff'
modified def Basis.ofEquivFun
modified theorem Basis.ofEquivFun_equivFun
modified theorem Basis.ofEquivFun_repr_apply
modified theorem Basis.repr_sum_self
modified theorem Basis.sum_equivFun
modified theorem Basis.sum_repr
modified theorem Module.card_fintype