Theorems · Theorem · group theory
zpow_add_one
∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a ^ (n + 1) = a ^ n * a- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- pow_zeroproof · cited by 1,094
- pow_oneproof · cited by 894
- pow_succproof · cited by 374
- zpow_natCastproof · cited by 271
- mul_inv_revproof · cited by 270
- pow_succ'proof · cited by 228
- zpow_negproof · cited by 198
- zpow_ofNatproof · cited by 144
- inv_mul_cancelproof · cited by 107
- zpow_negSuccproof · cited by 92
- inv_mul_cancel_rightproof · cited by 70
Cited by18
Results whose statement or proof uses this declaration.
- zpow_addproof · cited by 40
- zpow_right_strictMonoproof · cited by 5
- Equiv.Perm.SameCycle.apply_eq_self_iffproof · cited by 3
- zpow_sub_oneproof · cited by 3
- Set.pairwise_disjoint_Ioc_mul_zpowproof · cited by 2
- Subgroup.cyclic_of_minproof · cited by 2
- Representation.coeff_of_leftRegular_of_generatorproof · cited by 2
- Equiv.Perm.Basis.ofPermHomFun_commute_zpow_applyproof · cited by 2
- existsUnique_add_zpow_mem_Iocproof · cited by 2
- existsUnique_zpow_near_of_one_lt'proof · cited by 2
- zpow_right_strictAntiproof · cited by 2
- IsPGroup.smul_mul_inv_trivial_or_surjectiveproof · cited by 1