Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 08:42 7e37f208

View on Github →

feat(group_theory/perm/cycles): more lemmas (#8175)

Estimated changes

Modified src/group_theory/order_of_element.lean

added theorem nsmul_inj_mod

added theorem order_of_eq_zero_iff

added theorem pow_inj_iff_of_order_of_eq_zero

added theorem pow_inj_mod

Modified src/group_theory/perm/cycles.lean

modified theorem equiv.perm.cycle_factors_finset_eq_empty_iff

modified theorem equiv.perm.cycle_factors_finset_eq_singleton_iff

modified theorem equiv.perm.cycle_factors_finset_eq_singleton_self_iff

added theorem equiv.perm.cycle_factors_finset_mul_inv_mem_eq_sdiff

modified theorem equiv.perm.cycle_factors_finset_noncomm_prod

added theorem equiv.perm.cycle_factors_finset_one

added theorem equiv.perm.cycle_of_apply_apply_gpow_self

added theorem equiv.perm.cycle_of_apply_apply_pow_self

added theorem equiv.perm.cycle_of_apply_apply_self

added theorem equiv.perm.cycle_of_mem_cycle_factors_finset_iff

added theorem equiv.perm.cycle_of_mul_of_apply_right_eq_self

added theorem equiv.perm.disjoint.cycle_factors_finset_mul_eq_union

added theorem equiv.perm.disjoint.cycle_of_mul_distrib

added theorem equiv.perm.disjoint.disjoint_cycle_factors_finset

added theorem equiv.perm.disjoint_mul_inv_of_mem_cycle_factors_finset

added theorem equiv.perm.is_cycle.cycle_factors_finset_eq_singleton

added theorem equiv.perm.is_cycle.exists_pow_eq_one

added theorem equiv.perm.is_cycle.is_cycle_pow_pos_of_lt_prime_order

added theorem equiv.perm.is_cycle.mem_support_pos_pow_iff_of_lt_order_of

added theorem equiv.perm.is_cycle.pow_eq_one_iff

added theorem equiv.perm.is_cycle.pow_iff

added theorem equiv.perm.is_cycle.support_pow_eq_iff

added theorem equiv.perm.is_cycle_of_is_cycle_pow

added theorem equiv.perm.mem_cycle_factors_finset_support_le

added theorem equiv.perm.mem_support_cycle_of_iff

added theorem equiv.perm.nodup_of_pairwise_disjoint_cycles

added theorem equiv.perm.not_is_cycle_one

added theorem equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply

added theorem equiv.perm.same_cycle.nat''

added theorem equiv.perm.same_cycle.nat'

added theorem equiv.perm.same_cycle.nat

added theorem equiv.perm.same_cycle.nat_of_mem_support

added theorem equiv.perm.same_cycle_pow_left_iff

added theorem equiv.perm.support_cycle_of_eq_nil_iff

Modified src/group_theory/perm/support.lean

added theorem equiv.perm.disjoint.mono