Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems `root_add_root_mem_of_mem_of_mem`, `root_sub_mem_iff_root_add_mem`, `root_sub_root_mem_of_mem_of_mem`, `chainBotCoeff_mul_chainTopCoeff`, `isNotG2`	5
Total	5

RootPairing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chainBotCoeff_mul_chainTopCoeff` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Base.support` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set` `Set.instMembership` `Set.range`	`chainBotCoeff` `chainTopCoeff`	—	`chainBotCoeff_mul_chainTopCoeff.isNotG2` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Set.mem_range_self` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `sub_eq_add_neg` `neg_add_rev` `neg_neg` `neg_mem_range_root_iff` `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` `add_comm` `chainBotCoeff.congr_simp` `pairingIn_reflectionPerm_self_left` `instFaithfulSMulIntOfCharZero` `chainBotCoeff_reflectionPerm_right` `chainTopCoeff_reflectionPerm_right` `IsNotG2.toIsValuedIn` `chainBotCoeff_if_one_zero`

RootPairing.Base

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`root_add_root_mem_of_mem_of_mem` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `support` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`RootPairing.neg_mem_range_root_iff` `RingHomInvPair.ids` `RootPairing.root_reflectionPerm` `RootPairing.reflection_apply_self` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.neg_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval₃` `sub_zero` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `root_sub_root_mem_of_mem_of_mem` `Mathlib.Tactic.Contrapose.contrapose₄` `neg_neg` `neg_add_eq_sub` `neg_sub`
`root_sub_mem_iff_root_add_mem` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `support` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`root_add_root_mem_of_mem_of_mem` `root_sub_root_mem_of_mem_of_mem`
`root_sub_root_mem_of_mem_of_mem` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `support` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`lt_or_ge` `RootPairing.neg_mem_range_root_iff` `neg_sub` `RootPairing.root_sub_root_mem_of_pairingIn_pos` `Function.Embedding.injective` `sub_eq_zero` `left_eq_add` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_sub_assoc` `add_comm` `Function.instEmbeddingLikeEmbedding` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `sub_zero` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Module.NF.eq_cons_cons` `Mathlib.Tactic.Ring.neg_congr` `sub_notMem_range_root` `Mathlib.Tactic.Contrapose.contrapose₂` `FaithfulSMul.algebraMap_injective` `instFaithfulSMulIntOfCharZero` `RootPairing.algebraMap_pairingIn` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `Nat.instAtLeastTwoHAddOfNat` `eq_intCast` `Int.cast_ofNat` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SemilinearMapClass.toAddHomClass` `RootPairing.pairing_same` `LinearMap.congr_arg` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `neg_eq_zero` `sub_eq_zero_of_eq` `sub_ne_zero` `sub_neg_eq_add` `RootPairing.ne_zero` `CharZero.NeZero.two` `Module.IsReflexive.of_isPerfPair` `RootPairing.isPerfPair_toLinearMap` `Mathlib.Tactic.Contrapose.contrapose₄` `RootPairing.pairingIn_neg_two_neg_two_iff` `Module.IsReflexive.to_isTorsionFree` `RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic` `Int.instAddLeftMono` `covariant_swap_add_of_covariant_add` `Int.instZeroLEOneClass` `Int.instCharZero` `Int.cast_neg` `Int.cast_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Mathlib.Meta.NormNum.instAtLeastTwo` `pairingIn_le_zero_of_ne` `Mathlib.Tactic.Module.NF.sub_eq_eval₃` `Mathlib.Tactic.Module.NF.eq_const_cons`

RootPairing.chainBotCoeff_mul_chainTopCoeff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNotG2` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set` `Set.instMembership` `Set.range`	`RootPairing.IsNotG2`	—	`Module.IsReflexive.of_isPerfPair` `RootPairing.isPerfPair_toLinearMap` `IsAddTorsionFree.of_isTorsionFree` `Module.IsReflexive.to_isTorsionFree` `IsDomain.toIsCancelMulZero` `RootPairing.not_isG2_iff_isNotG2` `Submodule.mem_span_pair` `RootPairing.IsG2.span_eq_rootSpan_int` `Submodule.subset_span` `Set.mem_range_self` `two_nsmul` `RootPairing.nsmul_notMem_range_root` `Nat.instAtLeastTwoHAddOfNat` `neg_add_cancel` `RootPairing.ne_zero` `CharZero.NeZero.two` `add_eq_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `sub_eq_iff_eq_add` `sub_eq_add_neg` `neg_eq_iff_eq_neg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `add_zero` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `Mathlib.Tactic.Abel.subst_into_smul_upcast` `Mathlib.Tactic.Abel.term_smulg` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Abel.zero_smulg` `sub_eq_zero` `left_eq_add` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_sub_assoc` `add_comm` `sub_self` `eq_neg_add_iff_add_eq` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `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_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul` `instFaithfulSMulIntOfCharZero` `AddCommGroup.intIsScalarTower` `RootPairing.pairingIn_same` `Int.zsmul_eq_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `RootPairing.IsG2.pairingIn_mem_zero_one_three` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Function.Embedding.injective` `RootPairing.Base.root_ne_neg_of_ne` `instNontrivialOfCharZero`

---

← Back to Index