Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `equiv_of_mapsTo`, `mk'`, `mk''`, `mk'`	4
Theorems `ext`, `equiv_of_mapsTo_apply`, `equiv_of_mapsTo_symm_apply`, `ext`, `ext_iff`, `injOn_dualMap_subtype_span_root_coroot`, `isRootSystem_mk''`, `ext`	8
Total	12

RootPairing

Definitions

Name	Category	Theorems
`equiv_of_mapsTo` 📖	CompOp	2 math math: `equiv_of_mapsTo_apply`, `equiv_of_mapsTo_symm_apply`
`mk'` 📖	CompOp	—
`mk''` 📖	CompOp	1 math math: `isRootSystem_mk''`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_of_mapsTo_apply` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.preReflection` `Function.Embedding` `Function.instFunLikeEmbedding` `LinearMap` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `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` `LinearMap.flip` `Set.range` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	`Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv_of_mapsTo`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `Nat.instAtLeastTwoHAddOfNat`
`equiv_of_mapsTo_symm_apply` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.preReflection` `Function.Embedding` `Function.instFunLikeEmbedding` `LinearMap` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `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` `LinearMap.flip` `Set.range` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	`Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv_of_mapsTo`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `Nat.instAtLeastTwoHAddOfNat`
`ext` 📖	—	`toLinearMap` `root` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `coroot`	—	—	`Algebra.to_smulCommClass` `Equiv.Perm.ext` `Function.Embedding.injective` `root_reflectionPerm` `SMulCommClass.symm` `IsAddTorsionFree.of_isTorsionFree` `IsDomain.toIsCancelMulZero` `Function.Embedding.ext` `injOn_dualMap_subtype_span_root_coroot` `Set.mem_range_self` `smulCommClass_self` `RingHomCompTriple.ids` `Module.Dual.eq_of_preReflection_mapsTo'` `Set.finite_range` `Submodule.subset_span` `coroot_root_two` `mapsTo_reflection_root` `Nat.instAtLeastTwoHAddOfNat`
`ext_iff` 📖	mathematical	—	`toLinearMap` `root` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `coroot`	—	`Algebra.to_smulCommClass` `ext`
`injOn_dualMap_subtype_span_root_coroot` 📖	mathematical	—	`Set.InjOn` `Module.Dual` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Submodule.addCommMonoid` `Submodule.module` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.dualMap` `Submodule.subtype` `LinearMap.flip` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `toLinearMap` `coroot`	—	`smulCommClass_self` `SMulCommClass.symm` `Algebra.to_smulCommClass` `Module.injOn_dualMap_subtype_span_range_range` `Set.finite_range` `root_coroot_two` `mapsTo_reflection_root` `RingHomCompTriple.ids` `LinearEquiv.injective` `RingHomInvPair.ids` `isPerfPair_toLinearMap` `Set.mem_range_self`
`isRootSystem_mk''` 📖	mathematical	`DFunLike.coe` `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` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Function.Embedding` `Function.instFunLikeEmbedding` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.instAtLeastTwoHAddOfNat` `Set.MapsTo` `Module.End` `CommRing.toCommSemiring` `Module.preReflection` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap.flip` `Set.range` `Submodule.span` `Top.top` `Submodule` `Submodule.instTop` `AddGroupWithOne.toIntCast`	`IsRootSystem` `mk''`	—	`Algebra.to_smulCommClass` `Nat.instAtLeastTwoHAddOfNat` `SMulCommClass.symm` `rootSpan_eq_top_iff` `instIsAnisotropicOfIsCrystallographic`

RootPairing.IsRootSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`RootPairing.toLinearMap` `RootPairing.root`	—	—	`Algebra.to_smulCommClass` `LinearEquiv.injective` `RingHomInvPair.ids` `RootPairing.isPerfPair_toLinearMap` `Module.Dual.eq_of_preReflection_mapsTo` `Set.finite_range` `span_root_eq_top` `SMulCommClass.symm` `Nat.instAtLeastTwoHAddOfNat` `RootPairing.coroot_root_two` `LinearMap.flip.instIsPerfPair` `LinearMap.toPerfPair.congr_simp` `RootPairing.mapsTo_reflection_root` `RootPairing.ext` `le_antisymm`

RootSystem

Definitions

Name	Category	Theorems
`mk'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`RootPairing.toLinearMap` `RootPairing.root`	—	—	`RootPairing.IsRootSystem.ext`

---

← Back to Index