Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `flip`, `IsPerfPair`, `IsPerfectCompl`, `toPerfPair`	4
Theorems `coe_toLinearMap_flip`, `flip_apply`, `flip_flip`, `instIsPerfPair`, `isReflexive_of_equiv_dual_of_isReflexive`, `symm_flip`, `trans_dualMap_symm_flip`, `bijective_left`, `bijective_right`, `compl₁₂`, `dualEval`, `ext`, `ext_iff`, `flip`, `id`, `of_bijective`, `of_injective`, `of_injective'`, `flip`, `flip_iff`, `isCompl_left`, `isCompl_right`, `left_top_iff`, `right_top_iff`, `apply_symm_toPerfPair_self`, `apply_toPerfPair_flip`, `instIsPerfPair`, `toLinearMap_toPerfPair`, `toPerfPair_apply`, `of_isPerfPair`, `finrank_of_isPerfPair`, `dualAnnihilator_map_linearEquiv_flip_symm`, `dualCoannihilator_map_linearEquiv_flip`, `map_dualAnnihilator_linearEquiv_flip_symm`, `map_dualCoannihilator_linearEquiv_flip`	35
Total	39

LinearEquiv

Definitions

Name	Category	Theorems
`flip` 📖	CompOp	7 math math: `flip_apply`, `coe_toLinearMap_flip`, `flip_flip`, `symm_flip`, `Submodule.dualAnnihilator_map_linearEquiv_flip_symm`, `trans_dualMap_symm_flip`, `Submodule.map_dualAnnihilator_linearEquiv_flip_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toLinearMap_flip` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `flip` `LinearMap.flip`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`flip_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearEquiv` `RingHomInvPair.ids` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `flip`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`flip_flip` 📖	mathematical	—	`flip`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `ext` `LinearMap.ext`
`instIsPerfPair` 📖	mathematical	—	`LinearMap.IsPerfPair` `toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `bijective`
`isReflexive_of_equiv_dual_of_isReflexive` 📖	mathematical	—	`Module.IsReflexive` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `RingHomCompTriple.ids` `trans_dualMap_symm_flip` `bijective`
`symm_flip` 📖	mathematical	—	`symm` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `RingHomInvPair.ids` `flip` `trans` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomCompTriple.ids` `dualMap` `Module.evalEquiv`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`trans_dualMap_symm_flip` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `trans` `RingHomCompTriple.ids` `dualMap` `symm` `flip` `Module.Dual.eval`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `Module.apply_evalEquiv_symm_apply` `symm_apply_apply`

LinearMap

Definitions

Name	Category	Theorems
`IsPerfPair` 📖	CompData	15 math math: `IsPerfPair.restrict`, `IsPerfPair.of_injective`, `IsPerfPair.restrictScalars`, `IsPerfPair.of_bijective`, `RootPairing.isPerfPair_toLinearMap`, `IsPerfPair.compl₁₂`, `flip.instIsPerfPair`, `LinearEquiv.instIsPerfPair`, `IsPerfPair.id`, `Matrix.toPerfectPairing`, `IsPerfPair.congr`, `IsPerfPair.of_injective'`, `IsPerfPair.restrictScalars_of_field`, `IsPerfPair.flip`, `IsPerfPair.dualEval`
`IsPerfectCompl` 📖	CompData	4 math math: `IsPerfectCompl.flip_iff`, `RootPairing.IsBalanced.isPerfectCompl`, `IsPerfectCompl.left_top_iff`, `IsPerfectCompl.right_top_iff`
`toPerfPair` 📖	CompOp	23 math math: `apply_symm_toPerfPair_self`, `RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm`, `RootPairing.Hom.weight_coweight_transpose`, `RootPairing.toPerfPair_comp_root`, `RootPairing.corootSpan_map_flip_toPerfPair`, `IsPerfectCompl.isCompl_right`, `RootPairing.rootSpan_map_toPerfPair`, `RootPairing.corootSpan_dualAnnihilator_map_eq`, `RootPairing.toPerfPair_flip_comp_coroot`, `apply_toPerfPair_flip`, `RootPairing.Hom.weight_coweight_transpose_apply`, `RootPairing.ker_rootForm_eq_dualAnnihilator`, `RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'`, `RootPairing.toPerfPair_conj_reflection`, `RootPairing.toPerfPair_flip_conj_coreflection`, `RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm`, `RootPairing.rootSpan_dualAnnihilator_map_eq`, `toPerfPair_apply`, `toLinearMap_toPerfPair`, `RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'`, `RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection`, `RootPairing.ker_corootForm_eq_dualAnnihilator`, `IsPerfectCompl.isCompl_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_toPerfPair_self` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Algebra.id` `instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Module.Dual` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toPerfPair`	—	`Algebra.to_smulCommClass` `LinearEquiv.apply_symm_apply` `RingHomInvPair.ids`
`apply_toPerfPair_flip` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `instFunLike` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Algebra.id` `LinearEquiv` `RingHomInvPair.ids` `Module.Dual` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toPerfPair` `flip` `flip.instIsPerfPair`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `flip.instIsPerfPair` `apply_symm_toPerfPair_self`
`toLinearMap_toPerfPair` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toPerfPair` `LinearMap` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instFunLike`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids`
`toPerfPair_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearEquiv` `RingHomInvPair.ids` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toPerfPair` `LinearMap` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids`

LinearMap.IsPerfPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_left` 📖	mathematical	—	`Function.Bijective` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike`	—	`Algebra.to_smulCommClass`
`bijective_right` 📖	mathematical	—	`Function.Bijective` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike` `LinearMap.flip`	—	`Algebra.to_smulCommClass`
`compl₁₂` 📖	mathematical	—	`LinearMap.IsPerfPair` `LinearMap.compl₁₂` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `Function.Bijective.comp` `LinearEquiv.bijective` `bijective_left` `SMulCommClass.symm` `bijective_right`
`dualEval` 📖	mathematical	—	`LinearMap.IsPerfPair` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Module.Dual.eval`	—	`flip` `smulCommClass_self` `id`
`ext` 📖	—	—	—	—	`Algebra.to_smulCommClass` `SMulCommClass.symm`
`ext_iff` 📖	—	—	—	—	`Algebra.to_smulCommClass` `ext`
`flip` 📖	mathematical	—	`LinearMap.IsPerfPair` `LinearMap.flip` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`Algebra.to_smulCommClass` `bijective_right` `bijective_left`
`id` 📖	mathematical	—	`LinearMap.IsPerfPair` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.id` `LinearMap.addCommMonoid`	—	`Algebra.to_smulCommClass` `Function.bijective_id` `Module.bijective_dual_eval`
`of_bijective` 📖	mathematical	`Function.Bijective` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike`	`LinearMap.IsPerfPair`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `compl₁₂` `id`
`of_injective` 📖	mathematical	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearMap.instFunLike` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap.flip`	`LinearMap.IsPerfPair`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `LinearMap.flip_injective_iff₁` `FiniteDimensional.of_injective` `Subspace.instModuleDualFiniteDimensional` `LinearMap.flip_flip`
`of_injective'` 📖	mathematical	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearMap.instFunLike` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap.flip`	`LinearMap.IsPerfPair`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `flip` `of_injective`

LinearMap.IsPerfectCompl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip` 📖	mathematical	`LinearMap.IsPerfectCompl`	`LinearMap.flip` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.flip.instIsPerfPair`	—	`Algebra.to_smulCommClass` `LinearMap.flip.instIsPerfPair` `isCompl_right` `isCompl_left`
`flip_iff` 📖	mathematical	—	`LinearMap.IsPerfectCompl` `LinearMap.flip` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.flip.instIsPerfPair`	—	`Algebra.to_smulCommClass` `LinearMap.flip.instIsPerfPair` `flip`
`isCompl_left` 📖	mathematical	`LinearMap.IsPerfectCompl`	`IsCompl` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `Submodule.map` `Module.Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `LinearMap.toPerfPair` `Submodule.dualAnnihilator`	—	`Algebra.to_smulCommClass`
`isCompl_right` 📖	mathematical	`LinearMap.IsPerfectCompl`	`IsCompl` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `Submodule.map` `Module.Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `LinearMap.toPerfPair` `LinearMap.flip` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.flip.instIsPerfPair` `Submodule.dualAnnihilator`	—	`Algebra.to_smulCommClass`
`left_top_iff` 📖	mathematical	—	`LinearMap.IsPerfectCompl` `Top.top` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	—	`Algebra.to_smulCommClass` `eq_top_of_isCompl_bot` `RingHomSurjective.ids` `RingHomInvPair.ids` `LinearMap.flip.instIsPerfPair` `smulCommClass_self` `Submodule.map.congr_simp` `Submodule.dualAnnihilator_top` `Submodule.map_bot` `isCompl_right` `isCompl_top_bot`
`right_top_iff` 📖	mathematical	—	`LinearMap.IsPerfectCompl` `Top.top` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	—	`Algebra.to_smulCommClass` `LinearMap.flip.instIsPerfPair` `flip_iff` `left_top_iff`

LinearMap.flip

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsPerfPair` 📖	mathematical	—	`LinearMap.IsPerfPair` `LinearMap.flip` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`Algebra.to_smulCommClass` `LinearMap.IsPerfPair.flip`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_of_isPerfPair` 📖	mathematical	—	`finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Algebra.to_smulCommClass` `LinearEquiv.finrank_eq` `smulCommClass_self` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Finite.of_fintype` `LinearMap.flip.instIsPerfPair`

Module.IsReflexive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isPerfPair` 📖	mathematical	—	`Module.IsReflexive` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.flip.instIsPerfPair` `LinearMap.ext` `LinearMap.apply_toPerfPair_flip` `LinearEquiv.bijective`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dualAnnihilator_map_linearEquiv_flip_symm` 📖	mathematical	—	`dualAnnihilator` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `map` `Module.Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `LinearEquiv.flip` `dualCoannihilator`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive` `smulCommClass_self` `RingHomSurjective.ids` `SMulCommClass.symm` `map_dualCoannihilator_linearEquiv_flip` `LinearEquiv.coe_toLinearMap_flip` `LinearEquiv.flip_flip`
`dualCoannihilator_map_linearEquiv_flip` 📖	mathematical	—	`dualCoannihilator` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `map` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `RingHomSurjective.ids` `LinearMap.flip` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `Module.Dual` `LinearEquiv.symm` `dualAnnihilator`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `ext` `SMulCommClass.symm` `RingHomSurjective.ids` `smulCommClass_self` `RingHomSurjective.invPair`
`map_dualAnnihilator_linearEquiv_flip_symm` 📖	mathematical	—	`map` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `LinearEquiv.flip` `dualAnnihilator` `dualCoannihilator`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive` `RingHomSurjective.ids` `SMulCommClass.symm` `dualCoannihilator_map_linearEquiv_flip` `LinearEquiv.coe_toLinearMap_flip` `LinearEquiv.flip_flip`
`map_dualCoannihilator_linearEquiv_flip` 📖	mathematical	—	`map` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `RingHomSurjective.ids` `LinearMap.flip` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `Module.Dual` `dualCoannihilator` `dualAnnihilator` `LinearEquiv.symm`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive` `RingHomSurjective.ids` `SMulCommClass.symm` `dualCoannihilator_map_linearEquiv_flip` `LinearEquiv.coe_toLinearMap_flip` `LinearEquiv.flip_flip` `RingHomCompTriple.ids` `map_comp` `map.congr_simp` `LinearEquiv.symm_trans_self` `map_id` `LinearEquiv.self_trans_symm` `map_injective_of_injective` `LinearEquiv.injective`

---

← Back to Index