Documentation Verification Report

DualLattice

📁 Source: Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

Statistics

Metric	Count
Definitions `dualSubmodule`, `dualSubmoduleParing`, `dualSubmoduleToDual`	3
Theorems `dualSubmoduleParing_spec`, `dualSubmoduleToDual_apply_apply`, `dualSubmoduleToDual_injective`, `dualSubmodule_dualSubmodule_flip_of_basis`, `dualSubmodule_dualSubmodule_of_basis`, `dualSubmodule_flip_dualSubmodule_of_basis`, `dualSubmodule_span_of_basis`, `le_flip_dualSubmodule`, `mem_dualSubmodule`	9
Total	12

LinearMap.BilinForm

Definitions

Name	Category	Theorems
`dualSubmodule` 📖	CompOp	11 math math: `dualSubmoduleParing_spec`, `dualSubmoduleToDual_apply_apply`, `dualSubmoduleToDual_injective`, `dualSubmodule_span_of_basis`, `dualSubmodule_dualSubmodule_flip_of_basis`, `traceForm_dualSubmodule_adjoin`, `mem_dualSubmodule`, `Submodule.restrictScalars_traceDual`, `dualSubmodule_dualSubmodule_of_basis`, `dualSubmodule_flip_dualSubmodule_of_basis`, `le_flip_dualSubmodule`
`dualSubmoduleParing` 📖	CompOp	2 math math: `dualSubmoduleParing_spec`, `dualSubmoduleToDual_apply_apply`
`dualSubmoduleToDual` 📖	CompOp	2 math math: `dualSubmoduleToDual_apply_apply`, `dualSubmoduleToDual_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dualSubmoduleParing_spec` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `dualSubmoduleParing` `LinearMap` `Semifield.toCommSemiring` `RingHom.id` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `Submodule` `SetLike.instMembership` `Submodule.setLike` `dualSubmodule`	—	`Submodule.mem_one` `Subtype.prop`
`dualSubmoduleToDual_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Submodule.module` `Semiring.toModule` `LinearMap.instFunLike` `dualSubmodule` `Module.Dual` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `dualSubmoduleToDual` `dualSubmoduleParing`	—	`Algebra.to_smulCommClass`
`dualSubmoduleToDual_injective` 📖	mathematical	`Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SetLike.coe` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `Top.top` `Submodule.instTop`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `dualSubmodule` `Module.Dual` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike` `dualSubmoduleToDual`	—	`Algebra.to_smulCommClass` `LinearMap.ker_eq_bot` `Nondegenerate.ker_eq_bot` `LinearMap.ext_on` `dualSubmoduleParing_spec` `LinearMap.congr_fun`
`dualSubmodule_dualSubmodule_flip_of_basis` 📖	mathematical	`Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid`	`dualSubmodule` `flip` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.range` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.Basis.instFunLike`	—	`Nondegenerate.flip` `dualSubmodule_span_of_basis` `dualBasis_dualBasis_flip`
`dualSubmodule_dualSubmodule_of_basis` 📖	mathematical	`Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `IsSymm`	`dualSubmodule` `Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.Basis.instFunLike`	—	`dualSubmodule_span_of_basis` `dualBasis_dualBasis`
`dualSubmodule_flip_dualSubmodule_of_basis` 📖	mathematical	`Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid`	`dualSubmodule` `flip` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.range` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.Basis.instFunLike`	—	`dualSubmodule_span_of_basis` `Nondegenerate.flip` `dualBasis_flip_dualBasis`
`dualSubmodule_span_of_basis` 📖	mathematical	`Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid`	`dualSubmodule` `Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.Basis.instFunLike` `dualBasis`	—	`nonempty_fintype` `le_antisymm` `RingHomInvPair.ids` `Module.Basis.sum_repr` `sum_mem` `Submodule.addSubmonoidClass` `Submodule.mem_one` `Submodule.subset_span` `dualBasis_repr_apply` `algebraMap_smul` `Submodule.smul_mem` `Submodule.span_le` `Submodule.mem_span_range_iff_exists_fun` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `IsScalarTower.algebraMap_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `apply_dualBasis_left` `smul_eq_mul` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `RingHom.map_zero`
`le_flip_dualSubmodule` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `dualSubmodule` `flip` `Semifield.toCommSemiring` `Field.toSemifield`	—	`forall₂_comm`
`mem_dualSubmodule` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `dualSubmodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.one` `DFunLike.coe` `LinearMap` `Semifield.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module`	—	—

---

← Back to Index