Documentation Verification Report

Basis

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

Statistics

Metric	Count
Definitions `toBilin`, `toBilinHom`	2
Theorems `toQuadraticMap_surjective`, `add_toBilin`, `apply_linearCombination`, `apply_linearCombination'`, `map_finsuppSum`, `map_finsuppSum'`, `smul_toBilin`, `sum_polar_sub_repr_sq`, `sum_repr_sq_add_sum_repr_mul_polar`, `toBilinHom_apply`, `toBilin_apply`, `toQuadraticMap_toBilin`	12
Total	14

LinearMap.BilinMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toQuadraticMap_surjective` 📖	mathematical	—	`LinearMap.BilinMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap` `toQuadraticMap`	—	`Module.Free.exists_basis` `WellOrderingRel.isWellOrder` `QuadraticMap.toQuadraticMap_toBilin`

QuadraticMap

Definitions

Name	Category	Theorems
`toBilin` 📖	CompOp	5 math math: `smul_toBilin`, `toBilinHom_apply`, `add_toBilin`, `toBilin_apply`, `toQuadraticMap_toBilin`
`toBilinHom` 📖	CompOp	1 math math: `toBilinHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_toBilin` 📖	mathematical	—	`toBilin` `QuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAdd` `LinearMap.BilinMap` `LinearMap.instAdd` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `LinearMap.module`	—	`Module.Basis.ext` `lt_trichotomy` `toBilin_apply` `LT.lt.ne` `polar_add` `LT.lt.ne'` `LT.lt.not_gt` `add_zero`
`apply_linearCombination` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instMul` `Finset.sum` `Sym2` `Finset.filter` `Sym2.IsDiag` `Sym2.IsDiag.decidablePred` `Finset.sym2` `Finsupp.support` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Sym2.mul` `NonUnitalNonAssocCommSemiring.toCommMagma` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring` `Sym2.map` `Finsupp.instFunLike` `polarSym2`	—	`map_finsuppSum` `map_smul` `SemigroupAction.mul_smul` `Finsupp.sum_of_support_subset` `Finsupp.support_mul_subset_left` `zero_smul` `Finset.sum_congr` `Sym2.map_congr`
`apply_linearCombination'` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Sym2` `polarSym2` `Sym2.map` `Finsupp.sym2Mul` `CommSemiring.toCommMonoidWithZero` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instMul`	—	`map_finsuppSum'` `map_smul` `SemigroupAction.mul_smul` `Finsupp.sum_of_support_subset` `Finsupp.support_mul_subset_left` `zero_smul` `Finsupp.support_sym2Mul_subset` `Finset.sum_congr` `Sym2.map_congr`
`map_finsuppSum` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `Finsupp.sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Finset.sum` `Sym2` `Finset.filter` `Sym2.IsDiag` `Sym2.IsDiag.decidablePred` `Finset.sym2` `Finsupp.support` `polarSym2` `Sym2.map` `Finsupp` `Finsupp.instFunLike`	—	`map_sum`
`map_finsuppSum'` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `Finsupp.sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Finset.sum` `Sym2` `Finset.sym2` `Finsupp.support` `polarSym2` `Sym2.map` `Finsupp` `Finsupp.instFunLike`	—	`map_sum'`
`smul_toBilin` 📖	mathematical	—	`toBilin` `QuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass` `LinearMap.BilinMap` `LinearMap.instSMul` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `LinearMap.module` `DistribMulAction.toDistribSMul` `AddCommMonoid.toAddMonoid` `LinearMap.instDistribMulAction` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass`	—	`Module.Basis.ext` `IsScalarTower.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `lt_trichotomy` `toBilin_apply` `LT.lt.ne` `polar_smul` `LT.lt.ne'` `LT.lt.not_gt` `smul_zero`
`sum_polar_sub_repr_sq` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Sym2` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination` `polarSym2` `QuadraticMap` `instFunLike` `Sym2.map` `Module.Basis` `Module.Basis.instFunLike` `Finsupp.sym2Mul` `CommSemiring.toCommMonoidWithZero` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Finsupp.instMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`RingHomInvPair.ids` `apply_linearCombination'` `Module.Basis.linearCombination_repr`
`sum_repr_sq_add_sum_repr_mul_polar` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination` `QuadraticMap` `instFunLike` `Module.Basis` `Module.Basis.instFunLike` `Finsupp.instMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Finset.sum` `Sym2` `Finset.filter` `Sym2.IsDiag` `Sym2.IsDiag.decidablePred` `Finset.sym2` `Finsupp.support` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Sym2.mul` `NonUnitalNonAssocCommSemiring.toCommMagma` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring` `Sym2.map` `Finsupp.instFunLike` `polarSym2`	—	`RingHomInvPair.ids` `apply_linearCombination` `Module.Basis.linearCombination_repr`
`toBilinHom_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `QuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.BilinMap` `instAddCommMonoid` `LinearMap.addCommMonoid` `LinearMap.module` `instModuleOfSMulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `toBilinHom` `toBilin`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass`
`toBilin_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `LinearMap.BilinMap` `LinearMap.addCommMonoid` `LinearMap.module` `toBilin` `Module.Basis` `Module.Basis.instFunLike` `LinearOrder.toDecidableEq` `QuadraticMap` `instFunLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT` `polar` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Module.Basis.constr_basis`
`toQuadraticMap_toBilin` 📖	mathematical	—	`LinearMap.BilinMap.toQuadraticMap` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `toBilin`	—	`ext` `RingHomInvPair.ids` `Module.Basis.linearCombination_repr` `LinearMap.BilinMap.toQuadraticMap_apply` `Finsupp.linearCombination_apply` `Finsupp.sum.eq_1` `LinearMap.map_sum₂` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.map_smul₂` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `toBilin_apply` `smul_ite` `smul_zero` `Finset.sum_union` `Finset.disjoint_diag_offDiag` `Finset.sum_diag` `Finset.sum_ite_of_false` `Finset.mem_offDiag` `map_sum` `Finset.sum_filter` `polar_smul_right` `polar_smul_left` `map_smul` `SemigroupAction.mul_smul` `Finset.sum_sym2_filter_not_isDiag`

---

← Back to Index