Documentation Verification Report

Irreducible

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

Statistics

Metric	Count
Definitions `IsIrreducible`, `instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule`, `invtRootSubmodule`	3
Theorems `eq_top_of_invtSubmodule_coreflection`, `eq_top_of_invtSubmodule_reflection`, `mk'`, `nontrivial`, `nontrivial'`, `coe_bot`, `coe_top`, `eq_top_of_mem_invtSubmodule_of_forall_eq_univ`, `exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule`, `exists_form_eq_form_and_form_ne_zero`, `instIsIrreducibleFlip`, `instIsRootSystemOfNonemptyOfNeZeroOfNatOfIsIrreducible`, `instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule`, `bot_mem`, `eq_bot_iff`, `eq_top_iff`, `top_mem`, `invtSubmodule_reflection_of_invtSubmodule_coreflection`, `isIrreducible_iff`, `isIrreducible_iff_invtRootSubmodule`, `isSimpleModule_weylGroupRootRep`, `isSimpleModule_weylGroupRootRep_iff`, `mem_invtRootSubmodule_iff`, `span_orbit_eq_top`, `span_root_image_eq_top_of_forall_orthogonal`	25
Total	28

RootPairing

Definitions

Name	Category	Theorems
`IsIrreducible` 📖	CompData	7 math math: `IsNotG2.toIsIrreducible`, `isIrreducible_iff`, `IsIrreducible.mk'`, `instIsIrreducibleFlip`, `isIrreducible_iff_invtRootSubmodule`, `IsG2.toIsIrreducible`, `LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple`
`instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule` 📖	CompOp	5 math math: `invtRootSubmodule.eq_top_iff`, `invtRootSubmodule.eq_bot_iff`, `coe_bot`, `isIrreducible_iff_invtRootSubmodule`, `coe_top`
`invtRootSubmodule` 📖	CompOp	10 math math: `instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule`, `invtRootSubmodule.bot_mem`, `invtRootSubmodule.eq_top_iff`, `mem_invtRootSubmodule_iff`, `invtRootSubmodule.top_mem`, `invtRootSubmodule.eq_bot_iff`, `root_mem_submodule_iff_of_add_mem_invtSubmodule`, `coe_bot`, `isIrreducible_iff_invtRootSubmodule`, `coe_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtRootSubmodule` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `BoundedOrder.toOrderBot` `instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule` `Submodule.instBot`	—	—
`coe_top` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtRootSubmodule` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `BoundedOrder.toOrderTop` `instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule` `Submodule.instTop`	—	—
`eq_top_of_mem_invtSubmodule_of_forall_eq_univ` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `reflection` `Set.univ`	`Top.top` `Submodule.instTop`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Set.eq_empty_or_nonempty` `Algebra.to_smulCommClass` `RingHomSurjective.ids` `isPerfPair_toLinearMap` `corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'` `smulCommClass_self` `Submodule.map.congr_simp` `IsRootSystem.span_coroot_eq_top` `Submodule.dualAnnihilator_top` `Submodule.map_bot` `Submodule.disjoint_span_singleton'` `ne_zero` `Set.image_univ` `IsRootSystem.span_root_eq_top`
`exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `reflection`	`Disjoint` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set` `Set.instSingletonSet` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Preorder.toLE` `PartialOrder.toPreorder` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `coroot'`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `pairing_same` `Submodule.mem_invtSubmodule_reflection_iff`
`exists_form_eq_form_and_form_ne_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `InvariantForm.form` `Function.Embedding` `Function.instFunLikeEmbedding` `root`	—	`Nat.instAtLeastTwoHAddOfNat` `Submodule.span_le` `MulAction.mem_orbit_iff` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `weylGroup_apply_root` `Mathlib.Tactic.Push.not_and_eq` `Equiv.root_indexEquiv_eq_smul` `Subgroup.smul_def` `InvariantForm.apply_weylGroup_smul` `InvariantForm.apply_root_ne_zero` `span_orbit_eq_top`
`instIsIrreducibleFlip` 📖	mathematical	—	`IsIrreducible` `flip`	—	`IsIrreducible.nontrivial'` `IsIrreducible.nontrivial` `IsIrreducible.eq_top_of_invtSubmodule_coreflection` `IsIrreducible.eq_top_of_invtSubmodule_reflection`
`instIsRootSystemOfNonemptyOfNeZeroOfNatOfIsIrreducible` 📖	mathematical	—	`IsRootSystem`	—	`Nat.instAtLeastTwoHAddOfNat` `IsIrreducible.eq_top_of_invtSubmodule_reflection` `rootSpan_mem_invtSubmodule_reflection` `rootSpan_ne_bot` `IsIrreducible.eq_top_of_invtSubmodule_coreflection` `corootSpan_mem_invtSubmodule_coreflection` `corootSpan_ne_bot`
`instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule` 📖	mathematical	—	`Nontrivial` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtRootSubmodule`	—	`bot_ne_top` `Submodule.instNontrivial`
`invtSubmodule_reflection_of_invtSubmodule_coreflection` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `coreflection`	`reflection` `Submodule.map` `Module.Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `RingHomSurjective.ids` `LinearEquiv.symm` `LinearMap.toPerfPair` `toLinearMap` `isPerfPair_toLinearMap` `Submodule.dualAnnihilator`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `RingHomSurjective.ids` `isPerfPair_toLinearMap` `smulCommClass_self` `LinearEquiv.map_mem_invtSubmodule_iff` `LinearEquiv.symm_symm` `toPerfPair_conj_reflection` `Module.End.mem_invtSubmodule` `Submodule.map_le_iff_le_comap` `LE.le.trans` `Submodule.dualAnnihilator_map_dualMap_le` `Submodule.dualAnnihilator_anti`
`isIrreducible_iff` 📖	mathematical	—	`IsIrreducible` `Nontrivial` `Top.top` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	—	`RingHomInvPair.ids`
`isIrreducible_iff_invtRootSubmodule` 📖	mathematical	—	`IsIrreducible` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsSimpleOrder` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtRootSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule`	—	`instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule` `IsIrreducible.eq_top_of_invtSubmodule_reflection` `RingHomInvPair.ids` `mem_invtRootSubmodule_iff` `IsIrreducible.mk'` `IsSimpleOrder.eq_top_of_lt`
`isSimpleModule_weylGroupRootRep` 📖	mathematical	—	`IsSimpleModule` `MonoidAlgebra` `Aut` `Subgroup` `Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `weylGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidAlgebra.ring` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Representation.asModule` `AddCommGroup.toAddCommMonoid` `weylGroupRootRep` `Representation.instAddCommGroupAsModule` `Representation.instModuleMonoidAlgebraAsModule`	—	`IsIrreducible.nontrivial` `RingHomInvPair.ids` `isSimpleModule_weylGroupRootRep_iff` `IsIrreducible.eq_top_of_invtSubmodule_reflection`
`isSimpleModule_weylGroupRootRep_iff` 📖	mathematical	—	`IsSimpleModule` `MonoidAlgebra` `Aut` `Subgroup` `Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `weylGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidAlgebra.ring` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Representation.asModule` `AddCommGroup.toAddCommMonoid` `weylGroupRootRep` `Representation.instAddCommGroupAsModule` `Representation.instModuleMonoidAlgebraAsModule` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomInvPair.ids` `isSimpleModule_iff` `OrderIso.isSimpleOrder_iff` `weylGroup.induction` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `Module.End.invtSubmodule.one` `Module.End.invtSubmodule.comp` `Representation.mem_invtSubmodule` `IsSimpleOrder.eq_bot_or_eq_top` `Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice` `eq_or_ne` `reflection_mem_weylGroup`
`mem_invtRootSubmodule_iff` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtRootSubmodule` `Module.End.invtSubmodule` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `reflection`	—	`RingHomInvPair.ids`
`span_orbit_eq_top` 📖	mathematical	—	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `MulAction.orbit` `Aut` `Subgroup` `Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `weylGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Subgroup.instDistribMulActionSubtypeMem` `Equiv.instDistribMulActionAut` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Top.top` `Submodule` `Submodule.instTop`	—	`Nat.instAtLeastTwoHAddOfNat` `IsIrreducible.eq_top_of_invtSubmodule_reflection` `reflection_mem_weylGroup` `Module.End.span_orbit_mem_invtSubmodule` `Subgroup.smulCommClass_left` `Equiv.instSMulCommClassAut` `MulAction.mem_orbit_self` `ne_zero`
`span_root_image_eq_top_of_forall_orthogonal` 📖	mathematical	`Set.Nonempty` `IsOrthogonal`	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Top.top` `Submodule` `Submodule.instTop`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `Submodule.mem_invtSubmodule_reflection_of_mem` `Module.End.mem_invtSubmodule` `Submodule.mem_comap` `LinearEquiv.coe_coe` `Function.IsFixedPt.eq` `isFixedPt_reflection_of_isOrthogonal` `IsIrreducible.eq_top_of_invtSubmodule_reflection` `ne_zero`

RootPairing.IsIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_of_invtSubmodule_coreflection` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RootPairing.coreflection`	`Top.top` `Submodule.instTop`	—	—
`eq_top_of_invtSubmodule_reflection` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RootPairing.reflection`	`Top.top` `Submodule.instTop`	—	—
`mk'` 📖	mathematical	`Top.top` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	`RootPairing.IsIrreducible` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`RingHomInvPair.ids` `Module.nontrivial_dual_iff` `Module.Projective.of_free` `Module.Free.of_divisionRing` `Equiv.nontrivial` `Algebra.to_smulCommClass` `RootPairing.isPerfPair_toLinearMap` `smulCommClass_self` `RingHomSurjective.ids` `not_imp_comm` `Submodule.map_eq_top_iff` `RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection`
`nontrivial` 📖	mathematical	—	`Nontrivial`	—	—
`nontrivial'` 📖	mathematical	—	`Nontrivial`	—	—

RootPairing.invtRootSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_mem` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `RootPairing.invtRootSubmodule` `Bot.bot` `Submodule.instBot`	—	—
`eq_bot_iff` 📖	mathematical	—	`Bot.bot` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `RootPairing.invtRootSubmodule` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `BoundedOrder.toOrderBot` `RootPairing.instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule` `Submodule.setLike` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root`	—	`Nat.instAtLeastTwoHAddOfNat` `Module.IsReflexive.of_isPerfPair` `RootPairing.isPerfPair_toLinearMap` `RootPairing.ne_zero` `Subtype.mk_eq_bot_iff` `Submodule.eq_bot_iff` `Mathlib.Tactic.Contrapose.contrapose₂` `smulCommClass_self` `LinearMap.ext_on_range` `RootPairing.span_coroot'_eq_top` `LinearMap.map_eq_zero_iff` `Function.Bijective.injective` `Module.bijective_dual_eval` `RingHomInvPair.ids` `Mathlib.Tactic.Contrapose.contrapose₄` `Submodule.smul_mem_iff` `IsScalarTower.left` `Submodule.sub_mem_iff_right` `SMulCommClass.symm` `LinearMap.flip_apply` `RootPairing.reflection_apply` `RootPairing.mem_invtRootSubmodule_iff`
`eq_top_iff` 📖	mathematical	—	`Top.top` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `RootPairing.invtRootSubmodule` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `BoundedOrder.toOrderTop` `RootPairing.instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule` `Set` `Set.instHasSubset` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `SetLike.coe` `Submodule.setLike`	—	`RootPairing.IsRootSystem.span_root_eq_top` `IsScalarTower.left` `Submodule.span_coe_eq_restrictScalars` `Submodule.restrictScalars_self` `Submodule.span_mono`
`top_mem` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `RootPairing.invtRootSubmodule` `Top.top` `Submodule.instTop`	—	—

---

← Back to Index