Commit 2024-08-10 03:36 e15449d2

View on Github →

chore: split LinearAlgebra.Basis (#15639)

Estimated changes

added theorem Basis.coe_mk
added theorem Basis.coe_mkFinCons
added theorem Basis.coord_unitsSMul
added theorem Basis.finTwoProd_one
added theorem Basis.finTwoProd_zero
added def Basis.groupSMul
added theorem Basis.groupSMul_apply
added def Basis.isUnitSMul
added theorem Basis.isUnitSMul_apply
added theorem Basis.maximal
added theorem Basis.mem_center_iff
added theorem Basis.mk_apply
added theorem Basis.mk_coord_apply
added theorem Basis.mk_repr
added theorem Basis.prod_apply
added theorem Basis.prod_repr_inl
added theorem Basis.prod_repr_inr
added theorem Basis.repr_unitsSMul
added def Basis.unitsSMul
added theorem Basis.unitsSMul_apply
deleted theorem Basis.basis_singleton_iff
deleted theorem Basis.coe_finTwoProd_repr
deleted theorem Basis.coe_mk
deleted theorem Basis.coe_mkFinCons
deleted theorem Basis.coe_mkFinConsOfLE
deleted theorem Basis.coord_unitsSMul
deleted theorem Basis.finTwoProd_one
deleted theorem Basis.finTwoProd_zero
deleted def Basis.groupSMul
deleted theorem Basis.groupSMul_apply
deleted def Basis.isUnitSMul
deleted theorem Basis.isUnitSMul_apply
deleted theorem Basis.maximal
deleted theorem Basis.mem_center_iff
deleted theorem Basis.mk_apply
deleted theorem Basis.mk_coord_apply
deleted theorem Basis.mk_coord_apply_eq
deleted theorem Basis.mk_coord_apply_ne
deleted theorem Basis.mk_repr
deleted theorem Basis.prod_apply
deleted theorem Basis.prod_apply_inl_fst
deleted theorem Basis.prod_apply_inl_snd
deleted theorem Basis.prod_apply_inr_fst
deleted theorem Basis.prod_apply_inr_snd
deleted theorem Basis.prod_repr_inl
deleted theorem Basis.prod_repr_inr
deleted theorem Basis.repr_unitsSMul
deleted def Basis.unitsSMul
deleted theorem Basis.unitsSMul_apply