Documentation Verification Report

Descent

📁 Source: Mathlib/GroupTheory/Descent.lean

Statistics

Metric	Count
Definitions	0
Theorems `fg_of_descent`, `fg_of_descent'`, `fg_of_descent`, `fg_of_descent`, `fg_of_descent'`, `fg_of_descent`	6
Total	6

AddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_descent` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instAdd` `Real.instMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `Real.instSub` `AddMonoid.toNSMul`	`AddGroup.FG` `toAddGroup`	—	`QuotientAddGroup.mk_surjective` `Set.exists_max_image` `Set.toFinite` `Finite.Set.finite_range` `AddSubgroup.finite_quotient_of_finiteIndex` `Set.range_nonempty` `Set.eq_univ_iff_forall` `Set.mem_add` `Set.mem_range` `sub_eq_iff_eq_add'` `SetLike.mem_coe` `QuotientAddGroup.eq_iff_sub_mem` `AddSubgroup.normal_of_comm` `Function.surjInv_eq` `AddGroup.fg_of_descent` `AddSubgroup.mem_map` `AddSubgroup.nsmul_mem`
`fg_of_descent'` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Real.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `SubNegMonoid.toSub` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`AddGroup.FG` `toAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `fg_of_descent` `Mathlib.Meta.NormNum.isNat_le_true` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_descent` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.map` `Real` `Real.instLE` `Real.instZero` `Real.instLT` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `SetLike.coe` `AddSubgroup.instSetLike` `AddMonoidHom.range` `Set.univ` `Real.instAdd` `Real.instMul` `Real.instSub` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike`	`FG`	—	`Nat.instAtLeastTwoHAddOfNat` `Northcott.exists_min_image` `Set.nonempty_compl` `AddSubgroup.coe_top` `SetLike.coe_ne_coe` `Set.mem_add` `Set.mem_univ` `AddSubgroup.notMem_of_notMem_closure` `Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `Real.instZeroLEOneClass` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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_gt` `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` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `existsAddOfLE` `IsOrderedRing.toMulPosMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `le_of_lt` `AddSubgroup.add_mem` `AddSubgroup.mem_closure_of_mem` `AddSubgroup.mem_map_of_mem` `LT.lt.not_ge` `fg_iff` `Set.Finite.union` `Northcott.finite_le`

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_descent` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instAdd` `Real.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Real.instSub` `Monoid.toPow`	`Group.FG` `toGroup`	—	`QuotientGroup.mk_surjective` `Set.exists_max_image` `Set.toFinite` `Finite.Set.finite_range` `Subgroup.finite_quotient_of_finiteIndex` `Set.range_nonempty` `Set.eq_univ_iff_forall` `Set.mem_mul` `div_eq_iff_eq_mul'` `SetLike.mem_coe` `QuotientGroup.eq_iff_div_mem` `Subgroup.normal_of_comm` `Function.surjInv_eq` `Group.fg_of_descent` `Subgroup.mem_map` `Subgroup.pow_mem`
`fg_of_descent'` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Real.instAdd` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `DivInvMonoid.toDiv` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Group.FG` `toGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `fg_of_descent` `Mathlib.Meta.NormNum.isNat_le_true` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_descent` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.map` `Real` `Real.instLE` `Real.instZero` `Real.instLT` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid` `SetLike.coe` `Subgroup.instSetLike` `MonoidHom.range` `Set.univ` `Real.instAdd` `Real.instMul` `Real.instSub` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike`	`FG`	—	`Nat.instAtLeastTwoHAddOfNat` `Northcott.exists_min_image` `Set.nonempty_compl` `Subgroup.coe_top` `SetLike.coe_ne_coe` `Set.mem_mul` `Set.mem_univ` `Subgroup.notMem_of_notMem_closure` `Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `Real.instZeroLEOneClass` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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_gt` `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` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `le_of_lt` `Subgroup.mul_mem` `Subgroup.mem_closure_of_mem` `Subgroup.mem_map_of_mem` `LT.lt.not_ge` `fg_iff` `Set.Finite.union` `Northcott.finite_le`

---

← Back to Index