Documentation Verification Report

Submodule

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

Statistics

Metric	Count
Definitions `addSubgroupOfClosure`, `restrictScalars`, `inductionOnRankAux`	3
Theorems `addSubgroupOfClosure_apply`, `addSubgroupOfClosure_repr_apply`, `eq_bot_of_rank_eq_zero`, `mem_center_iff`, `mem_span_iff_repr_mem`, `mem_submodule_iff`, `mem_submodule_iff'`, `restrictScalars_apply`, `restrictScalars_repr_apply`	9
Total	12

Module.Basis

Definitions

Name	Category	Theorems
`addSubgroupOfClosure` 📖	CompOp	2 math math: `addSubgroupOfClosure_repr_apply`, `addSubgroupOfClosure_apply`
`restrictScalars` 📖	CompOp	3 math math: `restrictScalars_repr_apply`, `restrictScalars_apply`, `restrictScalars_toMatrix`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroupOfClosure_apply` 📖	mathematical	`AddSubgroup.closure` `AddCommGroup.toAddGroup` `Set.range` `DFunLike.coe` `Module.Basis` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`Submodule` `Int.instSemiring` `AddCommGroup.toIntModule` `SetLike.instMembership` `Submodule.setLike` `OrderIso` `AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderIso` `AddSubgroup.toIntSubmodule` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing` `addSubgroupOfClosure`	—	`restrictScalars_apply` `Int.instIsDomain` `AddCommGroup.intIsScalarTower`
`addSubgroupOfClosure_repr_apply` 📖	mathematical	`AddSubgroup.closure` `AddCommGroup.toAddGroup` `Set.range` `DFunLike.coe` `Module.Basis` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toIntModule` `SetLike.instMembership` `Submodule.setLike` `OrderIso` `AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderIso` `AddSubgroup.toIntSubmodule` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommGroup` `Int.instRing` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `addSubgroupOfClosure` `AddSubgroup.instSetLike`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.CompatibleSMul.finsupp_cod` `LinearMap.CompatibleSMul.intModule` `ext` `repr_self` `LinearMap.map_zero` `Finsupp.mapRange_single` `eq_intCast` `RingHom.instRingHomClass` `Int.cast_one` `addSubgroupOfClosure_apply` `DFunLike.congr_fun` `LinearMap.congr_fun`
`eq_bot_of_rank_eq_zero` 📖	mathematical	—	`Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	`Submodule.eq_bot_iff` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Fintype.linearIndependent_iff` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonFinOfNatNat` `smul_eq_zero` `Finset.sum_congr` `Finset.univ_unique` `Finset.sum_singleton` `one_ne_zero`
`mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.center` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Commute` `DFunLike.coe` `Module.Basis` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike`	—	`Commute.symm` `IsMulCentral.comm` `IsMulCentral.left_assoc` `IsMulCentral.right_assoc` `Set.center.eq_1` `Set.mem_setOf_eq` `RingHomInvPair.ids` `linearCombination_repr` `Finsupp.linearCombination_apply` `Finsupp.sum.eq_1` `commute_iff_eq` `Finset.sum_mul` `Finset.mul_sum` `Finset.sum_congr` `mul_smul_comm` `smul_mul_assoc` `Commute.eq` `Finset.smul_sum` `SMulCommClass.smul_comm` `Finset.sum_comm`
`mem_span_iff_repr_mem` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Module.Basis` `Ring.toSemiring` `instFunLike` `Set` `Set.instMembership` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr`	—	`RingHomInvPair.ids` `restrictScalars_repr_apply` `linearCombination_repr` `Finsupp.linearCombination_apply` `sum_mem` `Submodule.addSubmonoidClass` `algebraMap_smul` `Submodule.smul_mem` `Submodule.subset_span` `Set.mem_range_self`
`mem_submodule_iff` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Finsupp.sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Module.Basis` `Submodule.addCommMonoid` `Submodule.module` `instFunLike`	—	`RingHomSurjective.ids` `Submodule.range_subtype` `Submodule.map_top` `span_eq` `Submodule.map_span` `Set.range_comp` `Finsupp.range_linearCombination`
`mem_submodule_iff'` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Module.Basis` `Submodule.addCommMonoid` `Submodule.module` `instFunLike`	—	`mem_submodule_iff` `Finite.of_fintype` `Equiv.exists_congr_left` `Finsupp.sum_fintype` `zero_smul` `Finset.sum_congr`
`restrictScalars_apply` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Module.Basis` `Ring.toSemiring` `instFunLike` `Submodule.addCommMonoid` `Submodule.module` `restrictScalars`	—	`span_apply`
`restrictScalars_repr_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Module.Basis` `instFunLike` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `restrictScalars`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.CompatibleSMul.finsupp_cod` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `ext` `repr_self` `LinearMap.map_zero` `Finsupp.mapRange_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `restrictScalars_apply` `DFunLike.congr_fun` `LinearMap.congr_fun`

Submodule

Definitions

Name	Category	Theorems
`inductionOnRankAux` 📖	CompOp	—

---

← Back to Index