Relations

📁 Source: Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Relations.lean

Statistics

Metric	Count
Definitions Relations, Relations, Relations	3
Theorems isSl2Triple, lie_e_f_ne, lie_e_f_same, lie_h_e, lie_h_f	5
Total	8

AddCommGrpCat.Colimits

Definitions

Name	Category	Theorems
Relations 📖	CompOp	—

FirstOrder.Language

Definitions

Name	Category	Theorems
Relations 📖	CompOp	27 math math: LHom.id_onRelation, lhomWithConstants_onRelation, order.instSubsingleton, card_eq_card_functions_add_card_relations, empty.isFraisseLimit_of_countable_infinite, constantsOn_Relations, LHom.ofIsEmpty_onRelation, LHom.sumInr_onRelation, graph.instSubsingleton, LHom.sumElim_onRelation, order.instIsEmptyRelationsOfNatNat, withConstants_relMap_sumInl, BoundedFormula.mapTermRelEquiv_apply, orderLHom_onRelation, BoundedFormula.listEncode_sigma_injective, LHom.sumInl_onRelation, relMap_sumInl, LHom.sumMap_onRelation, BoundedFormula.listDecode_encode_list, BoundedFormula.mapTermRelEquiv_symm_apply, BoundedFormula.encoding_Γ, BoundedFormula.mapTermRel_mapTermRel, BoundedFormula.mapTermRel_id_id_id, card_relations_sum, relMap_sumInr, LHom.Injective.onRelation, skolem₁_Relations

Module

Definitions

Name	Category	Theorems
Relations 📖	CompData	—

RootPairing.GeckConstruction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSl2Triple 📖	mathematical	—	IsSl2Triple Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing h e f	—	Nat.instAtLeastTwoHAddOfNat Matrix.diagonal_apply_eq RootPairing.pairingIn_same instFaithfulSMulIntOfCharZero Int.cast_ofNat lie_e_f_same lie_h_e RootPairing.Base.cartanMatrixIn_apply_same zsmul_eq_mul nsmul_eq_mul lie_h_f neg_smul
lie_e_f_ne 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Ring.instBracket Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instFintypeSum Finset.Subtype.fintype e f Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	Matrix.ext Fintype.sum_sum_type Finset.sum_congr MulZeroClass.mul_zero Finset.sum_const_zero mul_ite ite_mul RootPairing.Base.cartanMatrix.congr_simp one_mul MulZeroClass.zero_mul Finset.sum_ite_eq' zero_add add_zero sub_zero Int.instAddLeftMono covariant_swap_add_of_covariant_add RootPairing.Base.sub_notMem_range_root RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.reflection_apply_self RootPairing.chainBotCoeff_reflectionPerm_right sub_self eq_or_ne Matrix.transpose_apply Pi.zero_apply Matrix.zero_apply RootPairing.Base.root_sub_root_mem_of_mem_of_mem Finset.sum_eq_single_of_mem Finset.mem_univ Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg add_comm RootPairing.chainBotCoeff_mul_chainTopCoeff Nat.cast_one RootPairing.Base.root_sub_mem_iff_root_add_mem Finset.sum_ite_of_false mul_one sub_eq_zero
lie_e_f_same 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Ring.instBracket Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instFintypeSum Finset.Subtype.fintype e f h	—	Module.IsReflexive.of_isPerfPair RootPairing.isPerfPair_toLinearMap IsAddTorsionFree.of_isTorsionFree Module.IsReflexive.to_isTorsionFree IsDomain.toIsCancelMulZero Matrix.ext Fintype.sum_sum_type Finset.sum_congr MulZeroClass.mul_zero Finset.sum_const_zero mul_ite ite_mul one_mul MulZeroClass.zero_mul Finset.sum_ite_eq' zero_add sub_self RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.reflection_apply_self sub_eq_add_neg AddRightCancelSemigroup.toIsRightCancelAdd Nat.instAtLeastTwoHAddOfNat RootPairing.ne_zero CharZero.NeZero.two AddLeftCancelSemigroup.toIsLeftCancelAdd mul_one add_zero add_neg_cancel RootPairing.chainBotCoeff_reflectionPerm_right eq_or_ne RootPairing.nsmul_notMem_range_root two_smul eq_sub_iff_add_eq RootPairing.ne_neg Finset.sum_eq_single_of_mem Finset.mem_univ RootPairing.Base.cartanMatrixIn_apply_same instFaithfulSMulIntOfCharZero Nat.abs_ofNat IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.cast_ofNat sub_zero RootPairing.pairingIn_same neg_add_rev smul_neg zero_sub neg_zero RootPairing.pairingIn_reflectionPerm_self_left Int.cast_neg add_sub_cancel Function.instEmbeddingLikeEmbedding add_sub_cancel_left Matrix.diagonal_apply_ne
lie_h_e 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Ring.instBracket Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instFintypeSum Finset.Subtype.fintype h e SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Matrix.addGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing RootPairing.Base.cartanMatrix	—	Matrix.ext Fintype.sum_sum_type Finset.sum_congr MulZeroClass.mul_zero Finset.sum_const_zero mul_ite MulZeroClass.zero_mul add_zero sub_self smul_zero Finset.sum_eq_ite Matrix.diagonal_apply_ne mul_one Matrix.diagonal_apply_eq ite_mul RootPairing.pairingIn.congr_simp RootPairing.pairingIn_reflectionPerm_self_left instFaithfulSMulIntOfCharZero Int.cast_neg mul_neg one_mul zero_add zero_sub smul_ite zsmul_eq_mul neg_zero neg_neg Finset.sum_ite_eq' sub_zero smul_add Finset.sum_sub_distrib Finset.sum_subset Finset.subset_univ IsDomain.to_noZeroDivisors eq_or_ne Finset.insert_eq_of_mem Finset.sum_singleton AddRightCancelSemigroup.toIsRightCancelAdd RootPairing.ne_zero CharZero.NeZero.two Finset.sum_insert ite_sub_ite RootPairing.pairingIn_eq_add_of_root_eq_add Int.cast_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
lie_h_f 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Ring.instBracket Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instFintypeSum Finset.Subtype.fintype h f SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Matrix.addGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing RootPairing.Base.cartanMatrix	—	Ring.lie_def mul_sub mul_assoc ω_mul_h ω_mul_f neg_sub neg_mul mul_neg sub_mul Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero lie_h_e Matrix.mul_smul Algebra.to_smulCommClass zsmul_eq_mul neg_smul ω_mul_ω one_mul

---

← Back to Index