IsValuedIn

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

Statistics

Metric	Count
Definitions IsCrystallographic, IsValuedIn, coroot'In, corootSpan, corootSpanMem, coxeterWeightIn, pairingIn, root'In, rootSpan, rootSpanMem	10
Theorems exists_value, trans, algebraMap_coroot'In_apply, algebraMap_coxeterWeightIn, algebraMap_pairingIn, algebraMap_pairingIn', algebraMap_root'In_apply, coroot'In_rootSpanMem_eq_pairingIn, coroot'_apply_apply_mem_of_mem_span, corootSpanMem_reflectionPerm_self, corootSpan_dualAnnihilator_map_eq, corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', corootSpan_map_flip_toPerfPair, corootSpan_mem_invtSubmodule_coreflection, corootSpan_ne_bot, exists_value, finrank_corootSpanIn, finrank_corootSpanIn_int, finrank_rootSpanIn, finrank_rootSpanIn_int, iInf_ker_coroot'_eq, iInf_ker_root'_eq, instFiniteSubtypeMemSubmoduleCorootSpanOfFinite, instFiniteSubtypeMemSubmoduleRootSpanOfFinite, instIsValuedIn, instIsValuedInFlip, instIsValuedInRatOfIsCrystallographic, isValuedIn_iff, isValuedIn_iff_mem_range, pairingIn_eq_add_of_root_eq_add, pairingIn_eq_add_of_root_eq_smul_add_smul, pairingIn_eq_zero_iff, pairingIn_rat, pairingIn_reflectionPerm, pairingIn_reflectionPerm_self_left, pairingIn_reflectionPerm_self_right, pairingIn_same, reflection_apply_root', root'In_corootSpanMem_eq_pairingIn, root'_apply_apply_mem_of_mem_span, rootSpanMem_reflectionPerm_self, rootSpan_dualAnnihilator_map_eq, rootSpan_dualAnnihilator_map_eq_iInf_ker_root', rootSpan_map_toPerfPair, rootSpan_mem_invtSubmodule_reflection, rootSpan_ne_bot, span_coroot'_eq_top, span_root'_eq_top, toLinearMap_apply_apply_mem_range_algebraMap	49
Total	59

RootPairing

Definitions

Name	Category	Theorems
IsCrystallographic 📖	MathDef	1 math math: LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem
IsValuedIn 📖	CompData	9 math math: EmbeddedG2.toIsValuedIn, IsG2.toIsValuedIn, instIsValuedInFlip, IsNotG2.toIsValuedIn, isValuedIn_iff_mem_range, isValuedIn_iff, instIsValuedInRatOfIsCrystallographic, IsValuedIn.trans, instIsValuedIn
coroot'In 📖	CompOp	4 math math: posRootForm_posForm_apply_apply, coroot'In_rootSpanMem_eq_pairingIn, PolarizationIn_apply, algebraMap_coroot'In_apply
corootSpan 📖	CompOp	26 math math: root'In_corootSpanMem_eq_pairingIn, Base.span_coroot_support, finrank_corootSpan_eq', range_polarization_domRestrict_le_span_coroot, finrank_range_polarization_eq_finrank_span_coroot, disjoint_corootSpan_ker_corootForm, finrank_rootSpan_map_polarization_eq_finrank_corootSpan, finrank_corootSpanIn_int, corootSpan_map_flip_toPerfPair, corootSpanMem_reflectionPerm_self, IsBalanced.isPerfectCompl, instFiniteSubtypeMemSubmoduleCorootSpanOfFinite, finrank_corootSpanIn, corootSpan_dualAnnihilator_map_eq, CoPolarizationIn_eq, corootSpan_mem_invtSubmodule_coreflection, orthogonal_corootSpan_eq, ker_rootForm_eq_dualAnnihilator, finrank_corootSpan_eq, corootSpan_dualAnnihilator_le_ker_rootForm, rootSpan_eq_top_iff, isCompl_corootSpan_ker_corootForm, CoPolarizationIn_apply, corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', range_polarizationIn_le_span_coroot, algebraMap_root'In_apply
corootSpanMem 📖	CompOp	2 math math: root'In_corootSpanMem_eq_pairingIn, corootSpanMem_reflectionPerm_self
coxeterWeightIn 📖	CompOp	6 math math: coxeterWeight_nonneg, coxeterWeightIn_eq_four_iff_not_linearIndependent, algebraMap_coxeterWeightIn, coxeterWeightIn_eq_zero_iff, coxeterWeightIn_mem_set_of_isCrystallographic, coxeterWeightIn_le_four
pairingIn 📖	CompOp	64 math math: GeckConstruction.h_def, RootPositiveForm.pairingIn_mul_eq_pairingIn_mul_swap, root'In_corootSpanMem_eq_pairingIn, Base.cartanMatrixIn_def, Base.injective_pairingIn, EmbeddedG2.pairingIn_threeShortAddLong_right, coroot'In_rootSpanMem_eq_pairingIn, Base.pairingIn_le_zero_of_ne, reflection_apply_root', pairingIn_pairingIn_mem_set_of_length_eq, zero_le_pairingIn_of_root_sub_mem, RootPositiveForm.posForm_apply_root_root_le_zero_iff, Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, pairingIn_pairingIn_mem_set_of_length_eq_of_ne, zero_lt_pairingIn_iff', pairingIn_eq_add_of_root_eq_add, pairingIn_eq_zero_of_add_notMem_of_sub_notMem, isG2_iff, zero_lt_pairingIn_iff, coxeterWeightIn_eq_zero_iff, EmbeddedG2.pairingIn_twoShortAddLong_left, algebraMap_pairingIn, pairingIn_reflectionPerm_self_left, EmbeddedG2.pairingIn_threeShortAddTwoLong_right, pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed, chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx, IsG2.pairingIn_mem_zero_one_three, EmbeddedG2.pairingIn_long_short, EmbeddedG2.pairingIn_threeShortAddLong_left, pairingIn_reflectionPerm_self_right, pairingIn_le_zero_iff, pairingIn_lt_zero_iff, forall_pairingIn_eq_swap_or, EmbeddedG2.pairingIn_short_long, pairingIn_eq_zero_iff, GeckConstruction.diagonal_elim_mem_span_h_iff, pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed', pairingIn_one_four_iff, pairingIn_neg_one_neg_four_iff, pairingIn_rat, EmbeddedG2.pairingIn_twoShortAddLong_right, pairingIn_reflectionPerm, pairingIn_le_zero_of_root_add_mem, EmbeddedG2.pairingIn_threeShortAddTwoLong_left, algebraMap_pairingIn', pairingIn_eq_add_of_root_eq_smul_add_smul, pairingIn_two_two_iff, chainBotCoeff_if_one_zero, chainTopCoeff_if_one_zero, Base.IsPos.exists_mem_support_pos_pairingIn, chainTopCoeff_sub_chainBotCoeff, RootPositiveForm.zero_lt_apply_root_root_iff, pairingIn_neg_two_neg_two_iff, isNotG2_iff, IsG2.exists_pairingIn_neg_three, EmbeddedG2.pairingIn_shortAddLong_left, pairingIn_pairingIn_mem_set_of_isCrystallographic, GeckConstruction.h_eq_diagonal, EmbeddedG2.pairingIn_shortAddLong_right, chainBotCoeff_sub_chainTopCoeff, pairingIn_same, Base.chainTopCoeff_eq_of_ne, baseOf_pairwise_pairing_le_zero, IsNotG2.pairingIn_mem_zero_one_two
root'In 📖	CompOp	3 math math: root'In_corootSpanMem_eq_pairingIn, CoPolarizationIn_apply, algebraMap_root'In_apply
rootSpan 📖	CompOp	38 math math: posRootForm_posForm_apply_apply, rootForm_restrict_nondegenerate_of_ordered, finrank_corootSpan_eq', rootSpan_dualAnnihilator_le_ker_rootForm, range_polarization_domRestrict_le_span_coroot, finrank_range_polarization_eq_finrank_span_coroot, coroot'In_rootSpanMem_eq_pairingIn, finrank_rootSpan_map_polarization_eq_finrank_corootSpan, instFiniteSubtypeMemSubmoduleRootSpanOfFinite, polarizationIn_Injective, finrank_rootSpanIn_int, PolarizationIn_eq, toLinearMap_apply_PolarizationIn, rootSpan_map_toPerfPair, IsBalanced.isPerfectCompl, prod_rootForm_smul_coroot_mem_range_domRestrict, IsG2.span_eq_rootSpan_int, algebraMap_rootFormIn, isCompl_rootSpan_ker_rootForm, PolarizationIn_apply, prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, range_polarizationIn, rootSpanMem_reflectionPerm_self, rootSpan_dualAnnihilator_map_eq_iInf_ker_root', algebraMap_coroot'In_apply, rootForm_restrict_nondegenerate_of_isAnisotropic, rootFormIn_self_smul_coroot, rootSpan_mem_invtSubmodule_reflection, finrank_corootSpan_eq, finrank_rootSpanIn, Base.span_root_support, rootSpan_dualAnnihilator_map_eq, rootSpan_eq_top_iff, disjoint_rootSpan_ker_rootForm, posRootForm_rootFormIn_posDef, ker_corootForm_eq_dualAnnihilator, range_polarizationIn_le_span_coroot, orthogonal_rootSpan_eq
rootSpanMem 📖	CompOp	4 math math: coroot'In_rootSpanMem_eq_pairingIn, prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, rootSpanMem_reflectionPerm_self, rootFormIn_self_smul_coroot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_coroot'In_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Module.Dual Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.id coroot'In coroot'	—	algebraMap_root'In_apply instIsValuedInFlip
algebraMap_coxeterWeightIn 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap coxeterWeightIn coxeterWeight	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass algebraMap_pairingIn
algebraMap_pairingIn 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap pairingIn pairing	—	exists_value
algebraMap_pairingIn' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap pairingIn	—	FaithfulSMul.algebraMap_injective RingHom.comp_apply IsScalarTower.algebraMap_eq algebraMap_pairingIn
algebraMap_root'In_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Module.Dual Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.id root'In root'	—	root'In.eq_1 Algebra.linearMap_apply LinearMap.restrictScalarsRange_apply Submodule.subtype_apply
coroot'In_rootSpanMem_eq_pairingIn 📖	mathematical	—	DFunLike.coe Module.Dual Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id coroot'In rootSpanMem pairingIn	—	—
coroot'_apply_apply_mem_of_mem_span 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root	Set Set.instMembership RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.id coroot'	—	RingHomSurjective.ids Set.ext Submodule.span_induction exists_value map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass map_add SemilinearMapClass.toAddHomClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul IsScalarTower.right Submodule.smul_mem
corootSpanMem_reflectionPerm_self 📖	mathematical	—	corootSpanMem DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubgroupClass.toNegMemClass AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.addSubgroupClass CommRing.toRing	—	AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass RingHomInvPair.ids coroot_reflectionPerm coreflection_apply_self
corootSpan_dualAnnihilator_map_eq 📖	mathematical	—	Submodule.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 LinearMap.toPerfPair toLinearMap isPerfPair_toLinearMap Submodule.dualAnnihilator corootSpan Submodule.dualCoannihilator Submodule.span Set.range coroot'	—	rootSpan_dualAnnihilator_map_eq
corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot' 📖	mathematical	—	Submodule.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 LinearMap.toPerfPair toLinearMap isPerfPair_toLinearMap Submodule.dualAnnihilator corootSpan iInf Submodule Submodule.instInfSet LinearMap.ker coroot'	—	rootSpan_dualAnnihilator_map_eq_iInf_ker_root'
corootSpan_map_flip_toPerfPair 📖	mathematical	—	Submodule.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 LinearMap.toPerfPair LinearMap.flip NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toLinearMap LinearMap.flip.instIsPerfPair isPerfPair_toLinearMap corootSpan Submodule.span Set.range coroot'	—	rootSpan_map_toPerfPair
corootSpan_mem_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 corootSpan	—	rootSpan_mem_invtSubmodule_reflection
corootSpan_ne_bot 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat rootSpan_ne_bot
exists_value 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap pairing	—	IsValuedIn.exists_value
finrank_corootSpanIn 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module	—	finrank_rootSpanIn instIsRootSystemFlip instIsValuedInFlip
finrank_corootSpanIn_int 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike corootSpan EuclideanDomain.toCommRing Field.toEuclideanDomain Int.instSemiring Submodule.addCommMonoid Submodule.addCommGroup Int.instRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	finrank_rootSpanIn_int instIsRootSystemFlip instIsValuedInFlip
finrank_rootSpanIn 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module	—	LinearMap.finrank_eq_of_isPerfPair isPerfPair_toLinearMap Submodule.span_span_of_tower IsRootSystem.span_root_eq_top IsRootSystem.span_coroot_eq_top toLinearMap_apply_apply_mem_range_algebraMap
finrank_rootSpanIn_int 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike rootSpan EuclideanDomain.toCommRing Field.toEuclideanDomain Int.instSemiring Submodule.addCommMonoid Submodule.addCommGroup Int.instRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	IsAddTorsionFree.of_isTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Submodule.finrank_span_eq_finrank_span Rat.nontrivial Algebra.instIsEpiOfIsDomainOfIsFractionRing Int.instIsDomain Rat.isFractionRing Module.Flat.instOfIsDedekindDomainOfIsTorsionFree IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Rat.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add AddCommGroup.intIsScalarTower instFiniteSubtypeMemSubmoduleRootSpanOfFinite finrank_rootSpanIn IsScalarTower.rat instIsValuedInRatOfIsCrystallographic
iInf_ker_coroot'_eq 📖	mathematical	—	iInf Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet LinearMap.ker NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id coroot' Submodule.dualCoannihilator Submodule.span Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Set.range	—	iInf_ker_root'_eq
iInf_ker_root'_eq 📖	mathematical	—	iInf Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet LinearMap.ker NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id root' Submodule.dualCoannihilator Submodule.span Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Set.range	—	Algebra.to_smulCommClass RingHomSurjective.ids RingHomInvPair.ids isPerfPair_toLinearMap rootSpan_dualAnnihilator_map_eq rootSpan_dualAnnihilator_map_eq_iInf_ker_root'
instFiniteSubtypeMemSubmoduleCorootSpanOfFinite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan Submodule.addCommMonoid Submodule.module	—	Module.Finite.span_of_finite Set.finite_range
instFiniteSubtypeMemSubmoduleRootSpanOfFinite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module	—	Module.Finite.span_of_finite Set.finite_range
instIsValuedIn 📖	mathematical	—	IsValuedIn Algebra.id CommRing.toCommSemiring	—	—
instIsValuedInFlip 📖	mathematical	—	IsValuedIn flip	—	isValuedIn_iff exists_value
instIsValuedInRatOfIsCrystallographic 📖	mathematical	—	IsValuedIn Rat.commRing	—	IsValuedIn.trans AddCommGroup.intIsScalarTower
isValuedIn_iff 📖	mathematical	—	IsValuedIn DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap pairing	—	—
isValuedIn_iff_mem_range 📖	mathematical	—	IsValuedIn Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap pairing	—	—
pairingIn_eq_add_of_root_eq_add 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	pairingIn Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	FaithfulSMul.algebraMap_injective map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass algebraMap_pairingIn pairing_eq_add_of_root_eq_add
pairingIn_eq_add_of_root_eq_smul_add_smul 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction	pairingIn Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul Algebra.id	—	FaithfulSMul.algebraMap_injective algebraMap_smul map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass algebraMap_pairingIn pairing_eq_add_of_root_eq_smul_add_smul
pairingIn_eq_zero_iff 📖	mathematical	—	pairingIn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Nat.instAtLeastTwoHAddOfNat FaithfulSMul.algebraMap_eq_zero_iff algebraMap_pairingIn pairing_eq_zero_iff
pairingIn_rat 📖	mathematical	—	pairingIn Rat.commRing instIsValuedInRatOfIsCrystallographic Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	instIsValuedInRatOfIsCrystallographic algebraMap_pairingIn' AddCommGroup.intIsScalarTower Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing eq_intCast RingHom.instRingHomClass
pairingIn_reflectionPerm 📖	mathematical	—	pairingIn DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm	—	FaithfulSMul.algebraMap_injective algebraMap_pairingIn pairing_reflectionPerm
pairingIn_reflectionPerm_self_left 📖	mathematical	—	pairingIn DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	FaithfulSMul.algebraMap_injective algebraMap_pairingIn pairing_reflectionPerm_self_left map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
pairingIn_reflectionPerm_self_right 📖	mathematical	—	pairingIn DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	FaithfulSMul.algebraMap_injective algebraMap_pairingIn pairing_reflectionPerm_self_right map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
pairingIn_same 📖	mathematical	—	pairingIn instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	FaithfulSMul.algebraMap_injective Nat.instAtLeastTwoHAddOfNat algebraMap_pairingIn pairing_same map_ofNat RingHom.instRingHomClass
reflection_apply_root' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reflection Function.Embedding Function.instFunLikeEmbedding root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction pairingIn	—	RingHomInvPair.ids reflection_apply_root algebraMap_pairingIn algebraMap_smul
root'In_corootSpanMem_eq_pairingIn 📖	mathematical	—	DFunLike.coe Module.Dual Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id root'In corootSpanMem pairingIn	—	—
root'_apply_apply_mem_of_mem_span 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding coroot	NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule LinearMap.range Semiring.toModule RingHom.id RingHomSurjective.ids Algebra.linearMap Module.Dual LinearMap.instFunLike root'	—	coroot'_apply_apply_mem_of_mem_span instIsValuedInFlip
rootSpanMem_reflectionPerm_self 📖	mathematical	—	rootSpanMem DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubgroupClass.toNegMemClass AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.addSubgroupClass CommRing.toRing	—	AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass RingHomInvPair.ids root_reflectionPerm reflection_apply_self
rootSpan_dualAnnihilator_map_eq 📖	mathematical	—	Submodule.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 LinearMap.toPerfPair toLinearMap flip isPerfPair_toLinearMap Submodule.dualAnnihilator rootSpan Submodule.dualCoannihilator Submodule.span Set.range root'	—	SetLike.coe_injective Algebra.to_smulCommClass RingHomSurjective.ids RingHomInvPair.ids isPerfPair_toLinearMap Set.ext SMulCommClass.symm Set.image_congr smulCommClass_self Submodule.coe_dualAnnihilator_span Submodule.coe_dualCoannihilator_span
rootSpan_dualAnnihilator_map_eq_iInf_ker_root' 📖	mathematical	—	Submodule.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 LinearMap.toPerfPair toLinearMap flip isPerfPair_toLinearMap Submodule.dualAnnihilator rootSpan iInf Submodule Submodule.instInfSet LinearMap.ker root'	—	SetLike.coe_injective Algebra.to_smulCommClass RingHomSurjective.ids RingHomInvPair.ids isPerfPair_toLinearMap Set.ext SMulCommClass.symm Set.image_congr smulCommClass_self Submodule.coe_dualAnnihilator_span Submodule.coe_iInf
rootSpan_map_toPerfPair 📖	mathematical	—	Submodule.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 LinearMap.toPerfPair toLinearMap isPerfPair_toLinearMap rootSpan Submodule.span Set.range root'	—	Algebra.to_smulCommClass RingHomSurjective.ids RingHomInvPair.ids isPerfPair_toLinearMap rootSpan.eq_1 Submodule.map_span Set.image_univ Set.image_comp LinearEquiv.coe_coe toPerfPair_comp_root
rootSpan_mem_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 reflection rootSpan	—	RingHomInvPair.ids Module.End.mem_invtSubmodule rootSpan.eq_1 Submodule.span_induction Submodule.mem_comap LinearEquiv.coe_coe reflection_apply_root Submodule.sub_mem Submodule.subset_span Set.mem_range_self Submodule.smul_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Submodule.add_mem map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
rootSpan_ne_bot 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat exists_ne_zero
span_coroot'_eq_top 📖	mathematical	—	Submodule.span 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 Set.range coroot' Top.top Submodule Submodule.instTop	—	span_root'_eq_top instIsRootSystemFlip
span_root'_eq_top 📖	mathematical	—	Submodule.span 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 Set.range root' Top.top Submodule Submodule.instTop	—	Algebra.to_smulCommClass RingHomSurjective.ids RingHomInvPair.ids isPerfPair_toLinearMap Submodule.map.congr_simp IsRootSystem.span_root_eq_top Submodule.map_top LinearEquiv.range
toLinearMap_apply_apply_mem_range_algebraMap 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan corootSpan	Subring CommRing.toRing Subring.instSetLike RingHom.range algebraMap DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id toLinearMap	—	LinearMap.BilinMap.apply_apply_mem_of_mem_span RingHomSurjective.ids IsScalarTower.to_smulCommClass' IsScalarTower.right smulCommClass_self RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Algebra.to_smulCommClass LinearMap.instIsScalarTower exists_value

RootPairing.IsValuedIn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_value 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RootPairing.pairing	—	—
trans 📖	mathematical	—	RootPairing.IsValuedIn	—	IsScalarTower.algebraMap_eq RootPairing.algebraMap_pairingIn

---

← Back to Index