Basic

📁 Source: Mathlib/LinearAlgebra/Basis/Basic.lean

Statistics

Metric	Count
Definitions `empty`, `emptyUnique`, `mk`, `singleton`, `span`, `uniqueBasis`	6
Theorems `basis_singleton_iff`, `coe_mk`, `coe_singleton`, `coe_span_apply`, `index_nonempty`, `isTorsionFree`, `linearIndepOn`, `linearIndependent`, `linearIndependent_coord`, `maximal`, `mem_span`, `mem_span_image`, `mem_span_repr_support`, `mk_apply`, `mk_coord_apply`, `mk_coord_apply_eq`, `mk_coord_apply_ne`, `mk_repr`, `ne_zero`, `repr_range`, `repr_support_subset_of_mem_span`, `self_mem_span_image`, `singleton_apply`, `singleton_repr`, `smul_eq_zero`, `span_apply`, `span_eq`, `span_neg`, `span_repr_eq_single`, `card_fintype`, `eq_top_iff_forall_basis_mem`	31
Total	37

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_fintype` 📖	mathematical	—	`Fintype.card` `Monoid.toPow` `Nat.instMonoid`	—	`Fintype.card_congr` `RingHomInvPair.ids` `Finite.of_fintype` `Fintype.card_pi` `Finset.prod_const`

Module.Basis

Definitions

Name	Category	Theorems
`empty` 📖	CompOp	1 math math: `Submodule.basisOfPid_bot`
`emptyUnique` 📖	CompOp	—
`mk` 📖	CompOp	—
`singleton` 📖	CompOp	7 math math: `OrthonormalBasis.toBasis_singleton`, `coe_singleton`, `ZSpan.coe_floor_self`, `singleton_repr`, `singleton_apply`, `LinearMap.toMatrix_singleton`, `ZSpan.coe_fract_self`
`span` 📖	CompOp	4 math math: `coe_span_apply`, `span_repr_eq_single`, `span_apply`, `span_neg`
`uniqueBasis` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_singleton_iff` 📖	mathematical	—	`Module.Basis` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`LinearIndependent.ne_zero` `IsDomain.toNontrivial` `linearIndependent` `Set.range_unique` `span_eq` `RingHomInvPair.ids` `add_smul` `smul_assoc` `IsScalarTower.left` `Finsupp.unique_ext` `smul_left_injective` `IsDomain.toIsCancelMulZero` `Finsupp.single_eq_same`
`coe_mk` 📖	mathematical	`LinearIndependent` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range`	`DFunLike.coe` `Module.Basis` `instFunLike`	—	`mk_apply`
`coe_singleton` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLike` `singleton` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`singleton_apply`
`coe_span_apply` 📖	mathematical	`LinearIndependent`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Module.Basis` `Submodule.addCommMonoid` `Submodule.module` `instFunLike` `span`	—	`Submodule.subset_span` `Set.mem_range_self` `span_apply`
`index_nonempty` 📖	—	—	—	—	`Nontrivial.exists_pair_ne` `RingHomInvPair.ids` `ext_elem_iff`
`isTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree`	—	`Function.Injective.moduleIsTorsionFree` `Finsupp.moduleIsTorsionFree` `instIsTorsionFree` `RingHomInvPair.ids` `LinearEquiv.injective` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`linearIndepOn` 📖	mathematical	—	`LinearIndepOn` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`LinearIndependent.linearIndepOn` `linearIndependent`
`linearIndependent` 📖	mathematical	—	`LinearIndependent` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`RingHomInvPair.ids` `repr_linearCombination`
`linearIndependent_coord` 📖	mathematical	—	`LinearIndependent` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `coord` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `linearIndependent_iff'ₛ` `LinearMap.coe_sum` `Finset.sum_congr` `Finset.sum_apply` `RingHomInvPair.ids` `repr_self` `Finsupp.single_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq`
`maximal` 📖	mathematical	—	`LinearIndependent.Maximal` `DFunLike.coe` `Module.Basis` `instFunLike` `linearIndependent`	—	`le_antisymm` `RingHomInvPair.ids` `linearCombination_repr` `injective` `LinearIndependent.linearCombination_ne_of_notMem_support` `Finsupp.linearCombination_apply` `Finsupp.sum_embDomain`
`mem_span` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`Submodule.span_mono` `RingHomInvPair.ids` `Set.image_subset_range` `mem_span_repr_support`
`mem_span_image` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `DFunLike.coe` `Module.Basis` `instFunLike` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr`	—	`RingHomInvPair.ids` `repr_support_subset_of_mem_span` `Submodule.span_mono` `Set.image_mono` `mem_span_repr_support`
`mem_span_repr_support` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `DFunLike.coe` `Module.Basis` `instFunLike` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr`	—	`RingHomInvPair.ids` `Finsupp.mem_span_image_iff_linearCombination` `linearCombination_repr`
`mk_apply` 📖	mathematical	`LinearIndependent` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range`	`DFunLike.coe` `Module.Basis` `instFunLike`	—	`Finsupp.linearCombination_single` `one_smul`
`mk_coord_apply` 📖	mathematical	`LinearIndependent` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `coord` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`eq_or_ne` `mk_coord_apply_eq` `mk_coord_apply_ne`
`mk_coord_apply_eq` 📖	mathematical	`LinearIndependent` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `coord` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Submodule.subset_span` `Set.mem_range_self` `LinearIndependent.repr_eq_single` `Finsupp.single_eq_same`
`mk_coord_apply_ne` 📖	mathematical	`LinearIndependent` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `coord` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Submodule.subset_span` `Set.mem_range_self` `LinearIndependent.repr_eq_single` `Finsupp.single_eq_of_ne'`
`mk_repr` 📖	mathematical	`LinearIndependent` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `LinearMap` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `LinearIndependent.repr` `Submodule.mem_top`	—	`RingHomInvPair.ids`
`ne_zero` 📖	—	—	—	—	`LinearIndependent.ne_zero` `linearIndependent`
`repr_range` 📖	mathematical	—	`LinearMap.range` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `repr` `Finsupp.supported` `Set.univ`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `RingHomSurjective.invPair` `LinearEquiv.range` `Finsupp.supported_univ`
`repr_support_subset_of_mem_span` 📖	mathematical	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `DFunLike.coe` `Module.Basis` `instFunLike`	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr`	—	`RingHomInvPair.ids` `Finsupp.mem_span_image_iff_linearCombination` `repr_linearCombination` `Finsupp.mem_supported`
`self_mem_span_image` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `DFunLike.coe` `Module.Basis` `instFunLike` `Set` `Set.instMembership`	—	`RingHomInvPair.ids` `repr_self` `Finsupp.support_single_ne_zero` `NeZero.one` `Finset.coe_singleton`
`singleton_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLike` `singleton` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `apply_eq_iff`
`singleton_repr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instAddCommMonoid` `Semiring.toModule` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `singleton`	—	`RingHomInvPair.ids` `Unique.eq_default` `Finsupp.single_eq_same`
`smul_eq_zero` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isTorsionFree` `smul_eq_zero` `IsDomain.toIsCancelMulZero`
`span_apply` 📖	mathematical	`LinearIndependent`	`DFunLike.coe` `Module.Basis` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `instFunLike` `span` `Submodule.subset_span` `Set.mem_range_self`	—	`Submodule.subset_span` `Set.mem_range_self` `mk_apply` `linearIndependent_span`
`span_eq` 📖	mathematical	—	`Submodule.span` `Set.range` `DFunLike.coe` `Module.Basis` `instFunLike` `Top.top` `Submodule` `Submodule.instTop`	—	`eq_top_iff` `mem_span`
`span_neg` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `Submodule.span` `Set.range` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearIndependent.neg` `map` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `LinearEquiv.trans` `Submodule.addCommGroup` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.neg` `LinearEquiv.ofEq`	—	`eq_of_apply_eq` `LinearIndependent.neg` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Submodule.subset_span` `Set.mem_range_self` `span_apply` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`span_repr_eq_single` 📖	mathematical	`LinearIndependent` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.subset_span` `Set.mem_range_self`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `span` `Finsupp.single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `LinearEquiv.eq_symm_apply` `linearIndependent_span` `repr_symm_apply` `Finsupp.linearCombination_single` `one_smul`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_iff_forall_basis_mem` 📖	mathematical	—	`Top.top` `Submodule` `instTop` `SetLike.instMembership` `setLike` `DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike`	—	`Module.Basis.span_eq` `IsScalarTower.left` `span_coe_eq_restrictScalars` `restrictScalars_self` `span_mono`

---

← Back to Index