Documentation Verification Report

WeylGroup

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

Statistics

Metric	Count
Definitions `weylGroup`, `ofIdx`, `weylGroupCorootRep`, `weylGroupRootRep`, `weylGroupToPerm`	5
Theorems `apply_weylGroup_smul`, `range_weylGroupToPerm`, `range_weylGroup_coweightHom`, `range_weylGroup_weightHom`, `reflection_mem_weylGroup`, `induction`, `induction'`, `ofIdx_smul`, `weylGroup_apply_root`, `weylGroup_toSubmonoid`	10
Total	15

RootPairing

Definitions

Name	Category	Theorems
`weylGroup` 📖	CompOp	11 math math: `weylGroup_toSubmonoid`, `span_orbit_eq_top`, `range_weylGroup_coweightHom`, `weylGroup_apply_root`, `isSimpleModule_weylGroupRootRep`, `InvariantForm.apply_weylGroup_smul`, `isSimpleModule_weylGroupRootRep_iff`, `reflection_mem_weylGroup`, `range_weylGroupToPerm`, `weylGroup.ofIdx_smul`, `range_weylGroup_weightHom`
`weylGroupCorootRep` 📖	CompOp	—
`weylGroupRootRep` 📖	CompOp	2 math math: `isSimpleModule_weylGroupRootRep`, `isSimpleModule_weylGroupRootRep_iff`
`weylGroupToPerm` 📖	CompOp	2 math math: `weylGroup_apply_root`, `range_weylGroupToPerm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_weylGroupToPerm` 📖	mathematical	—	`MonoidHom.range` `Aut` `Subgroup` `Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `weylGroup` `Subgroup.toGroup` `Equiv` `Equiv.Perm.permGroup` `weylGroupToPerm` `Subgroup.closure` `Set.range` `reflectionPerm`	—	`Subgroup.closure_eq_of_le` `MonoidHom.restrict_range` `reflection_mem_weylGroup` `Subgroup.closure_induction''` `Subgroup.subset_closure` `Set.mem_range_self` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass` `Equiv.reflection_inv` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `map_mul` `MonoidHomClass.toMulHomClass` `Subgroup.mul_mem`
`range_weylGroup_coweightHom` 📖	mathematical	—	`MonoidHom.range` `Aut` `Subgroup` `Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `weylGroup` `Subgroup.toGroup` `MulOpposite` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `MulOpposite.instGroup` `LinearEquiv.automorphismGroup` `MonoidHom.restrict` `Monoid.toMulOneClass` `Equiv.instMonoid` `MulOpposite.instMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Equiv.coweightHom` `Subgroup.closure` `Set.range` `MulOpposite.op` `coreflection`	—	`RingHomInvPair.ids` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Subgroup.closure_eq_of_le` `MonoidHom.restrict_range` `reflection_mem_weylGroup` `Equiv.reflection_coweightEquiv` `Subgroup.closure_induction''` `Subgroup.subset_closure` `Set.mem_range_self` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Equiv.reflection_inv` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `map_mul` `MonoidHomClass.toMulHomClass` `Subgroup.mul_mem`
`range_weylGroup_weightHom` 📖	mathematical	—	`MonoidHom.range` `Aut` `Subgroup` `Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `weylGroup` `Subgroup.toGroup` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.restrict` `Monoid.toMulOneClass` `Equiv.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Equiv.weightHom` `Subgroup.closure` `Set.range` `reflection`	—	`RingHomInvPair.ids` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Subgroup.closure_eq_of_le` `MonoidHom.restrict_range` `Set.image_congr` `reflection_mem_weylGroup` `Equiv.reflection_weightEquiv` `Subgroup.closure_induction''` `Subgroup.subset_closure` `Set.mem_range_self` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Equiv.reflection_inv` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `map_mul` `MonoidHomClass.toMulHomClass` `Subgroup.mul_mem`
`reflection_mem_weylGroup` 📖	mathematical	—	`Aut` `Subgroup` `Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `weylGroup` `Equiv.reflection`	—	`Subgroup.subset_closure` `Set.mem_range_self`
`weylGroup_apply_root` 📖	mathematical	—	`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` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `MulOneClass.toMulOne` `SubmonoidClass.toMulOneClass` `Monoid.toMulOneClass` `Equiv.instMonoid` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `weylGroupToPerm`	—	`Hom.root_weightMap_apply`
`weylGroup_toSubmonoid` 📖	mathematical	—	`Subgroup.toSubmonoid` `Aut` `Equiv.instGroup` `weylGroup` `Submonoid.closure` `Monoid.toMulOneClass` `Equiv.instMonoid` `Set.range` `Equiv.reflection`	—	`Set.ext` `Equiv.reflection_inv` `weylGroup.eq_1` `Subgroup.closure_toSubmonoid` `Set.union_self`

RootPairing.InvariantForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_weylGroup_smul` 📖	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` `form` `RootPairing.Aut` `Subgroup` `RootPairing.Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `RootPairing.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` `RootPairing.Equiv.instDistribMulActionAut`	—	`RootPairing.weylGroup.induction` `RootPairing.reflection_mem_weylGroup` `apply_reflection_reflection` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `one_smul` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Submonoid.mul_mem` `SemigroupAction.mul_smul`

RootPairing.weylGroup

Definitions

Name	Category	Theorems
`ofIdx` 📖	CompOp	1 math math: `ofIdx_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction` 📖	—	`RootPairing.Equiv.reflection` `RootPairing.reflection_mem_weylGroup` `RootPairing.Aut` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `RootPairing.Equiv.instGroup` `OneMemClass.one_mem` `Subgroup` `Subgroup.instSetLike` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `RootPairing.weylGroup` `MulOne.toMul` `MulOneClass.toMulOne` `RootPairing.Equiv.instMonoid` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SetLike.instMembership`	—	—	`RootPairing.reflection_mem_weylGroup` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `RootPairing.weylGroup_toSubmonoid` `Submonoid.closure_induction` `Submonoid.subset_closure`
`induction'` 📖	—	`RootPairing.Equiv.reflection` `RootPairing.reflection_mem_weylGroup` `RootPairing.Aut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RootPairing.Equiv.instMonoid` `MulMemClass.mul_mem` `Subgroup` `RootPairing.Equiv.instGroup` `Subgroup.instSetLike` `SubmonoidClass.toMulMemClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `RootPairing.weylGroup` `SetLike.instMembership`	—	—	`RootPairing.reflection_mem_weylGroup` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `induction` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `sq` `mul_eq_one_iff_inv_eq` `RootPairing.Equiv.reflection_inv`
`ofIdx_smul` 📖	mathematical	—	`RootPairing.Aut` `Subgroup` `RootPairing.Equiv.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `RootPairing.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` `RootPairing.Equiv.instDistribMulActionAut` `ofIdx` `RootPairing.Equiv.instMonoid` `RootPairing.Equiv.reflection`	—	—

---

← Back to Index