Documentation Verification Report

SMul

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

Statistics

Metric	Count
Definitions `groupSMul`, `instMulAction`, `instSMul`, `isUnitSMul`, `unitsSMul`	5
Theorems `coe_smul`, `coord_unitsSMul`, `groupSMul_apply`, `groupSMul_span_eq_top`, `instIsScalarTower`, `instSMulCommClass`, `isUnitSMul_apply`, `repr_isUnitSMul`, `repr_smul`, `repr_unitsSMul`, `smul_apply`, `smul_eq_map`, `unitsSMul_apply`, `units_smul_span_eq_top`	14
Total	19

Module.Basis

Definitions

Name	Category	Theorems
`groupSMul` 📖	CompOp	1 math math: `groupSMul_apply`
`instMulAction` 📖	CompOp	—
`instSMul` 📖	CompOp	12 math math: `instIsScalarTower`, `Algebra.smul_leftMulMatrix`, `AffineBasis.basisOf_smul`, `repr_smul`, `smul_det`, `LinearMap.toMatrix_smulBasis_left`, `coe_smul`, `LinearMap.toMatrix_smulBasis_right`, `smul_eq_map`, `toMatrix_smul_left`, `smul_apply`, `instSMulCommClass`
`isUnitSMul` 📖	CompOp	5 math math: `repr_isUnitSMul`, `ZSpan.smul`, `det_isUnitSMul`, `isUnitSMul_apply`, `toMatrix_isUnitSMul`
`unitsSMul` 📖	CompOp	8 math math: `det_unitsSMul`, `orientation_unitsSMul`, `orientation_neg_single`, `det_unitsSMul_self`, `repr_unitsSMul`, `unitsSMul_apply`, `coord_unitsSMul`, `toMatrix_unitsSMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`coord_unitsSMul` 📖	mathematical	—	`coord` `CommSemiring.toSemiring` `unitsSMul` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Units.instSMul` `LinearMap.instSMul` `instDistribSMul` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Units.instInv`	—	`ext` `smulCommClass_self` `Submodule.mem_top` `inv_mul_cancel` `one_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `RingHomInvPair.ids` `repr_self` `Finsupp.single_apply` `mul_one` `MulZeroClass.mul_zero`
`groupSMul_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `instFunLike` `groupSMul` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mk_apply` `LinearIndependent.group_smul` `linearIndependent` `Eq.ge` `groupSMul_span_eq_top` `span_eq`
`groupSMul_span_eq_top` 📖	mathematical	`Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Pi.smul'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`eq_top_iff` `Submodule.mem_span` `Submodule.smul_mem` `inv_smul_smul` `smul_one_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `Module.Basis` `instSMul`	—	`DFunLike.ext` `smul_assoc` `RingHomInvPair.ids`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `Module.Basis` `instSMul`	—	`DFunLike.ext` `SMulCommClass.smul_comm` `RingHomInvPair.ids`
`isUnitSMul_apply` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`DFunLike.coe` `Module.Basis` `instFunLike` `isUnitSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`unitsSMul_apply`
`repr_isUnitSMul` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `isUnitSMul` `Units` `Units.instSMul` `Algebra.toSMul` `Algebra.id` `Units.instInv` `IsUnit.unit`	—	`repr_unitsSMul`
`repr_smul` 📖	mathematical	—	`repr` `Module.Basis` `instSMul` `LinearEquiv.trans` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.symm` `DistribMulAction.toLinearEquiv`	—	`RingHomInvPair.ids`
`repr_unitsSMul` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `unitsSMul` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units.instSMul` `Algebra.toSMul` `Algebra.id` `Units.instInv`	—	`smulCommClass_self` `coord_unitsSMul`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `instFunLike` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`smul_eq_map` 📖	mathematical	—	`LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Basis` `instSMul` `LinearEquiv.automorphismGroup` `LinearEquiv.applyDistribMulAction` `LinearEquiv.apply_smulCommClass'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommMonoid.toAddMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `map`	—	`RingHomInvPair.ids` `LinearEquiv.apply_smulCommClass'` `IsScalarTower.left`
`unitsSMul_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `instFunLike` `unitsSMul` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`mk_apply` `LinearIndependent.units_smul` `linearIndependent` `Eq.ge` `units_smul_span_eq_top` `span_eq`
`units_smul_span_eq_top` 📖	mathematical	`Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Pi.smul'` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`groupSMul_span_eq_top` `Units.instIsScalarTower` `IsScalarTower.left`

---

← Back to Index