Documentation Verification Report

BaseExists

📁 Source: Mathlib/LinearAlgebra/RootSystem/BaseExists.lean

Statistics

Metric	Count
Definitions `mk'`	1
Theorems `baseOf_pairwise_pairing_le_zero`, `baseOf_root_eq_baseOf_coroot`, `coroot_mem_or_neg_mem_closure_of_root`, `eq_baseOf_iff`, `eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure`, `linearIndepOn_root_baseOf`, `linearIndepOn_root_baseOf'`, `ncard_eq_finrank_of_linearIndepOn_of`, `nonempty_base`	9
Total	10

RootPairing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseOf_pairwise_pairing_le_zero` 📖	mathematical	—	`Set.Pairwise` `IsAddIndecomposable.baseOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `pairingIn` `Int.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing`	—	`IsAddIndecomposable.pairwise_baseOf_sub_notMem` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `Mathlib.Tactic.Contrapose.contrapose₂` `root_sub_root_mem_of_pairingIn_pos`
`baseOf_root_eq_baseOf_coroot` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Rat.addMonoid` `AddMonoidHom.instFunLike` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `coroot`	`IsAddIndecomposable.baseOf` `Rat.linearOrder`	—	`subset_antisymm` `Set.instAntisymmSubset` `instIsRootSystemFlip` `instIsValuedInFlip` `instFlipIsReduced` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`coroot_mem_or_neg_mem_closure_of_root` 📖	mathematical	`LinearIndepOn` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`coroot`	—	`Module.exists_dual_forall_apply_eq_one` `LinearIndependent.restrict_scalars'` `IsScalarTower.rat` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsScalarTower.right` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure` `AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure` `Rat.instIsOrderedAddMonoid` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `ne_zero` `CharZero.NeZero.two` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `Nat.instAtLeastTwoHAddOfNat` `instIsValuedInRatOfIsCrystallographic` `Rat.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `RootPositiveForm.zero_lt_posForm_apply_root` `Rat.cast_div` `Rat.cast_ofNat` `algebraMap_rootFormIn` `eq_ratCast` `RingHom.instRingHomClass` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `instIsAnisotropicOfIsCrystallographic` `coroot_eq_polarizationEquiv_apply_root` `Rat.cast_smul_eq_qsmul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearEquiv.symm_apply_apply` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `LT.lt.ne'` `baseOf_root_eq_baseOf_coroot` `IsAddIndecomposable.mem_or_neg_mem_closure_baseOf` `coroot_reflectionPerm` `coreflection_apply_self`
`eq_baseOf_iff` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Rat.addMonoid` `AddMonoidHom.instFunLike` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsAddIndecomposable.baseOf` `Rat.linearOrder` `LinearIndepOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`linearIndepOn_root_baseOf` `IsAddIndecomposable.mem_or_neg_mem_closure_baseOf` `Rat.instIsOrderedAddMonoid` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure`
`eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure` 📖	mathematical	`LinearIndepOn` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `Rat.addMonoid` `AddMonoidHom.instFunLike`	`IsAddIndecomposable.baseOf` `Rat.linearOrder`	—	`AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure` `Rat.instIsOrderedAddMonoid` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `ne_zero` `CharZero.NeZero.two` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `IsAddIndecomposable.mem_or_neg_mem_closure_baseOf` `ncard_eq_finrank_of_linearIndepOn_of` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `linearIndepOn_root_baseOf` `AddSubmonoid.closure_induction` `Int.cast_one` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `Int.cast_zero` `map_add` `AddMonoidHomClass.toAddHomClass` `Int.cast_add` `Int.cast_neg` `map_neg` `neg_neg` `Rat.instAddLeftMono` `Set.eq_of_subset_of_ncard_le` `le_refl` `Set.toFinite` `Subtype.finite`
`linearIndepOn_root_baseOf` 📖	mathematical	—	`LinearIndepOn` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `IsAddIndecomposable.baseOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Rat.linearOrder` `Rat.addMonoid`	—	`Subtype.finite` `le_antisymm` `Submodule.span_mono` `Function.instEmbeddingLikeEmbedding` `Submodule.span_le` `Submodule.span_span_of_tower` `AddCommGroup.intIsScalarTower` `Submodule.coe_toAddSubgroup` `Submodule.span_int_eq_addSubgroupClosure` `AddSubgroup.closure_image_isAddIndecomposable_baseOf` `Rat.instIsOrderedAddMonoid` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `Submodule.subset_span` `AddSubgroup.subset_closure` `Function.Injective.mem_set_image` `Submodule.injective_subtype` `RingHomSurjective.ids` `Submodule.map_coe` `SetLike.mem_coe` `Submodule.map_span` `Set.image_univ` `Set.image_comp` `Set.image_congr` `Set.ext` `eq_top_iff` `LinearMap.map_le_map_iff'` `Submodule.ker_subtype` `Submodule.map_top` `Submodule.range_subtype` `LinearIndependent.of_comp` `linearIndepOn_root_baseOf'` `instIsDomain` `Rat.instIsStrictOrderedRing` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsScalarTower.rat` `instIsValuedInRatOfIsCrystallographic` `le_refl` `finrank_rootSpanIn` `Module.finrank_eq_nat_card_basis` `commRing_strongRankCondition` `Rat.nontrivial` `Set.range_comp` `Submodule.span_image` `IsRootSystem.span_root_eq_top` `linearIndependent_iff_card_eq_finrank_span` `CommRing.orzechProperty` `Set.finrank.eq_1` `finrank_top` `Fintype.card_eq_nat_card`
`linearIndepOn_root_baseOf'` 📖	mathematical	—	`LinearIndepOn` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `IsAddIndecomposable.baseOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidHomClass.toAddMonoidHom` `Module.Dual` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `RingHom` `RingHom.instFunLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`	—	`Algebra.charZero_of_charZero` `IsStrictOrderedRing.toCharZero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `RingHomCompTriple.ids` `posRootForm_eq` `posRootForm_rootFormIn_posDef` `Submodule.subset_span` `Set.mem_range_self` `RootPositiveForm.posForm_apply_root_root_le_zero_iff` `algebraMap_pairingIn'` `AddCommGroup.intIsScalarTower` `eq_intCast` `RingHom.instRingHomClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `baseOf_pairwise_pairing_le_zero` `LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero` `LinearMap.linearIndependent_iff_of_disjoint` `Submodule.ker_subtype`
`ncard_eq_finrank_of_linearIndepOn_of` 📖	mathematical	`LinearIndepOn` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.ncard` `Module.finrank`	—	`IsRootSystem.span_root_eq_top` `Submodule.span_le` `Submodule.span_span_of_tower` `AddCommGroup.intIsScalarTower` `Submodule.subset_span` `Submodule.span_int_eq_addSubgroupClosure` `AddSubgroup.le_closure_toAddSubmonoid` `AddSubgroupClass.toNegMemClass` `AddSubgroup.instAddSubgroupClass` `Subtype.finite` `Set.toFinite` `Set.ncard_eq_toFinset_card` `Set.toFinite_toFinset` `Set.toFinset_card` `Module.finrank_eq_card_basis` `commRing_strongRankCondition`
`nonempty_base` 📖	mathematical	—	`Base` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Module.exists_dual_forall_apply_ne_zero` `NoMinOrder.infinite` `instNoMinOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.nontrivial` `Nat.instAtLeastTwoHAddOfNat` `ne_zero` `CharZero.NeZero.two` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `linearIndepOn_root_baseOf` `IsAddIndecomposable.mem_or_neg_mem_closure_baseOf` `Rat.instIsOrderedAddMonoid` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self`

RootPairing.Base

Definitions

Name	Category	Theorems
`mk'` 📖	CompOp	—

---

← Back to Index