CartanMatrix

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

Statistics

Metric	Count
Definitions cartanMatrix, cartanMatrixIn, equivOfCartanMatrixEq	3
Theorems abs_cartanMatrix_apply, algebraMap_cartanMatrixIn_apply, apply_mem_range_root_of_cartanMatrixEq, cartanMatrixIn_apply_same, cartanMatrixIn_def, cartanMatrixIn_mul_diagonal_eq, cartanMatrixIn_nondegenerate, cartanMatrix_apply_eq_zero_iff, cartanMatrix_apply_eq_zero_iff_pairing, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_same, cartanMatrix_eq_neg_chainTopCoeff, cartanMatrix_le_zero_of_ne, cartanMatrix_map_abs, cartanMatrix_mem_of_ne, cartanMatrix_nondegenerate, exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, induction_on_cartanMatrix, injective_pairingIn	19
Total	22

RootPairing.Base

Definitions

Name	Category	Theorems
cartanMatrix 📖	CompOp	14 math math: cartanMatrix_map_abs, cartanMatrix_apply_eq_zero_iff, cartanMatrix_nondegenerate, RootPairing.GeckConstruction.lie_h_e, cartanMatrix_apply_eq_zero_iff_pairing, cartanMatrix_apply_same, cartanMatrix_le_zero_of_ne, cartanMatrix_eq_neg_chainTopCoeff, RootPairing.GeckConstruction.lie_h_f, RootPairing.GeckConstruction.lie_e_lie_f_apply, cartanMatrix_mem_of_ne, abs_cartanMatrix_apply, cartanMatrix_apply_eq_zero_iff_symm, RootPairing.GeckConstruction.e_lie_u
cartanMatrixIn 📖	CompOp	5 math math: cartanMatrixIn_def, algebraMap_cartanMatrixIn_apply, cartanMatrixIn_nondegenerate, cartanMatrixIn_apply_same, cartanMatrixIn_mul_diagonal_eq
equivOfCartanMatrixEq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_cartanMatrix_apply 📖	mathematical	—	abs instLatticeInt Int.instAddGroup cartanMatrix Finset SetLike.instMembership Finset.instSetLike support	—	eq_or_ne Nat.instAtLeastTwoHAddOfNat cartanMatrixIn_apply_same instFaithfulSMulIntOfCharZero Nat.abs_ofNat IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing zero_sub Int.instIsOrderedAddMonoid cartanMatrix_le_zero_of_ne
algebraMap_cartanMatrixIn_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap cartanMatrixIn RootPairing.pairing Finset SetLike.instMembership Finset.instSetLike support	—	RootPairing.algebraMap_pairingIn
apply_mem_range_root_of_cartanMatrixEq 📖	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset SetLike.instMembership Finset.instSetLike support Equiv Equiv.instEquivLike Set Set.instMembership Set.range cartanMatrix	—	—	RingHomInvPair.ids RingHomCompTriple.ids RootPairing.algebraMap_pairingIn map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass Module.Basis.ext toWeightBasis_apply induction_reflect RootPairing.root_reflectionPerm RootPairing.reflection_apply_self map_neg LinearEquiv.congr_fun Set.mem_range_self
cartanMatrixIn_apply_same 📖	mathematical	—	cartanMatrixIn instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	FaithfulSMul.algebraMap_injective Nat.instAtLeastTwoHAddOfNat RootPairing.pairingIn_same map_ofNat RingHom.instRingHomClass
cartanMatrixIn_def 📖	mathematical	—	cartanMatrixIn RootPairing.pairingIn Finset SetLike.instMembership Finset.instSetLike support	—	—
cartanMatrixIn_mul_diagonal_eq 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike support Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Finset.Subtype.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.map cartanMatrixIn DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass LinearMap RingHom.id AddCommGroup.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPairing.InvariantForm.form Function.Embedding Function.instFunLikeEmbedding RootPairing.root Matrix.smul Algebra.toSMul Algebra.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat LinearEquiv RingHomInvPair.ids Matrix.addCommMonoid Algebra.to_smulCommClass LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.toMatrix toWeightBasis	—	Matrix.ext Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.mul_diagonal algebraMap_cartanMatrixIn_apply LinearMap.BilinForm.toMatrix_apply toWeightBasis_apply RootPairing.InvariantForm.two_mul_apply_root_root
cartanMatrixIn_nondegenerate 📖	mathematical	—	Matrix.Nondegenerate Finset SetLike.instMembership Finset.instSetLike support Subtype.finite Finite.of_fintype cartanMatrixIn	—	Nat.instAtLeastTwoHAddOfNat Subtype.finite Finite.of_fintype RootPairing.rootForm_nondegenerate RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass Matrix.Nondegenerate.smul_iff two_ne_zero LinearMap.BilinForm.nondegenerate_toMatrix_iff Matrix.nondegenerate_iff_det_ne_zero Matrix.det_diagonal Finset.prod_ne_zero_iff IsDomain.toNontrivial IsDomain.to_noZeroDivisors RootPairing.pairing_same FaithfulSMul.algebraMap_eq_zero_iff RingHom.map_det RingHom.mapMatrix_apply Matrix.Nondegenerate.mul_iff_right cartanMatrixIn_mul_diagonal_eq
cartanMatrix_apply_eq_zero_iff 📖	mathematical	—	cartanMatrix Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Finset SetLike.instMembership Finset.instSetLike support	—	cartanMatrix_eq_neg_chainTopCoeff neg_eq_zero RootPairing.chainTopCoeff_eq_zero_iff linearIndependent_pair_of_ne
cartanMatrix_apply_eq_zero_iff_pairing 📖	mathematical	—	cartanMatrix RootPairing.pairing Finset SetLike.instMembership Finset.instSetLike support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	cartanMatrix.eq_1 cartanMatrixIn_def FaithfulSMul.algebraMap_injective instFaithfulSMulIntOfCharZero RootPairing.algebraMap_pairingIn map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cartanMatrix_apply_eq_zero_iff_symm 📖	mathematical	—	cartanMatrix	—	Module.IsReflexive.of_isPerfPair RootPairing.isPerfPair_toLinearMap RootPairing.pairing_eq_zero_iff CharZero.NeZero.two Module.IsReflexive.to_isTorsionFree
cartanMatrix_apply_same 📖	mathematical	—	cartanMatrix	—	cartanMatrixIn_apply_same instFaithfulSMulIntOfCharZero
cartanMatrix_eq_neg_chainTopCoeff 📖	mathematical	—	cartanMatrix RootPairing.chainTopCoeff Finset SetLike.instMembership Finset.instSetLike support	—	cartanMatrix.eq_1 cartanMatrixIn_def neg_eq_iff_eq_neg chainTopCoeff_eq_of_ne
cartanMatrix_le_zero_of_ne 📖	mathematical	—	cartanMatrix	—	pairingIn_le_zero_of_ne
cartanMatrix_map_abs 📖	mathematical	—	Matrix.map Finset SetLike.instMembership Finset.instSetLike support cartanMatrix abs instLatticeInt Int.instAddGroup Matrix Matrix.sub instOfNatAtLeastTwo Matrix.instNatCastOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Nat.instAtLeastTwoHAddOfNat	—	Matrix.ext Nat.instAtLeastTwoHAddOfNat abs_cartanMatrix_apply Matrix.ofNat_apply Nat.cast_ite CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero
cartanMatrix_mem_of_ne 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet cartanMatrix	—	Module.IsReflexive.of_isPerfPair RootPairing.isPerfPair_toLinearMap RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic cartanMatrix_le_zero_of_ne Int.instCharZero Nat.instAtLeastTwoHAddOfNat not_linearIndependent_iff Multiset.nodup_cons Finset.sum_congr Finset.sum_cons Finsupp.single_eq_same Finsupp.single_eq_of_ne add_zero RootPairing.pairingIn_neg_one_neg_four_iff Module.IsReflexive.to_isTorsionFree instFaithfulSMulIntOfCharZero neg_smul smul_neg one_smul zero_add Multiset.sum_singleton neg_add_cancel NeZero.one instNontrivialOfCharZero linearIndepOn_root RootPairing.pairingIn_reflectionPerm_self_left RootPairing.pairingIn_same
cartanMatrix_nondegenerate 📖	mathematical	—	Matrix.Nondegenerate Finset SetLike.instMembership Finset.instSetLike support Int.instCommRing Subtype.finite cartanMatrix	—	cartanMatrixIn_nondegenerate CharZero.NeZero.two instFaithfulSMulIntOfCharZero Int.instIsDomain RootPairing.instIsAnisotropicOfIsCrystallographic
exists_mem_span_pairingIn_ne_zero_and_pairwise_ne 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.range Finset Finset.instSetLike support AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra Pairwise Function.onFun	—	Module.Dual.exists_forall_mem_ne_zero_of_forall_exists Finite.instSum Subtype.finite Finite.instProd CharZero.infinite exists_mem_support_pos_pairingIn_ne_zero Submodule.subset_span RootPairing.pairingIn_eq_zero_iff instFaithfulSMulIntOfCharZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors CharZero.NeZero.two Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq injective_pairingIn
induction_on_cartanMatrix 📖	—	—	—	—	Submodule.ne_bot_iff Submodule.subset_span Set.image_congr Function.instEmbeddingLikeEmbedding RootPairing.ne_zero CharZero.NeZero.two Mathlib.Tactic.Contrapose.contrapose₁ LinearIndependent.notMem_span_image instNontrivialOfCharZero LinearIndepOn.linearIndependent linearIndepOn_root LinearMap.mem_ker Mathlib.Tactic.Contrapose.contrapose₂ Submodule.span_induction cartanMatrix_apply_eq_zero_iff_symm cartanMatrix_apply_eq_zero_iff_pairing map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass add_zero map_add SemilinearMapClass.toAddHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass IsDomain.to_noZeroDivisors RingHomInvPair.ids forall_mem_support_invtSubmodule_iff Module.End.mem_invtSubmodule Submodule.mem_comap LinearEquiv.coe_coe RootPairing.reflection_apply Submodule.sub_mem Submodule.smul_mem zero_smul AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass RootPairing.IsIrreducible.eq_top_of_invtSubmodule_reflection
injective_pairingIn 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing Finset SetLike.instMembership Finset.instSetLike support	—	exists_root_eq_sum_int FaithfulSMul.algebraMap_injective instFaithfulSMulIntOfCharZero RootPairing.algebraMap_pairingIn map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Algebra.to_smulCommClass LinearMap.map_smul_of_tower LinearMap.CompatibleSMul.intModule zsmul_eq_mul eq_intCast Finset.sum_subtype Matrix.vecMul_eq_sum Finset.sum_apply Matrix.vecMul_injective_iff Matrix.linearIndependent_rows_of_det_ne_zero Int.instIsDomain Finite.of_fintype Matrix.nondegenerate_iff_det_ne_zero cartanMatrix_nondegenerate Function.Embedding.apply_eq_iff_eq

---

← Back to Index