Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-03-16 09:30
0c2c2bdd
View on Github →
feat(group_theory/perm/cycles): cycle_factors (
#815
)
Estimated changes
Created
src/group_theory/perm/cycles.lean
added
theorem
equiv.perm.apply_eq_self_iff_of_same_cycle
added
def
equiv.perm.cycle_factors
added
def
equiv.perm.cycle_factors_aux
added
def
equiv.perm.cycle_of
added
theorem
equiv.perm.cycle_of_apply
added
theorem
equiv.perm.cycle_of_apply_of_not_same_cycle
added
theorem
equiv.perm.cycle_of_apply_of_same_cycle
added
theorem
equiv.perm.cycle_of_apply_self
added
theorem
equiv.perm.cycle_of_cycle
added
theorem
equiv.perm.cycle_of_gpow_apply_self
added
theorem
equiv.perm.cycle_of_inv
added
theorem
equiv.perm.cycle_of_one
added
theorem
equiv.perm.cycle_of_pow_apply_self
added
theorem
equiv.perm.is_cycle_cycle_of
added
theorem
equiv.perm.same_cycle.refl
added
theorem
equiv.perm.same_cycle.symm
added
theorem
equiv.perm.same_cycle.trans
added
def
equiv.perm.same_cycle
added
theorem
equiv.perm.same_cycle_apply
added
theorem
equiv.perm.same_cycle_cycle
added
theorem
equiv.perm.same_cycle_inv
added
theorem
equiv.perm.same_cycle_inv_apply
added
theorem
equiv.perm.same_cycle_of_is_cycle
Renamed
src/group_theory/perm.lean
to
src/group_theory/perm/sign.lean
added
theorem
equiv.perm.card_support_swap_mul
added
theorem
equiv.perm.disjoint.symm
added
def
equiv.perm.disjoint
added
theorem
equiv.perm.disjoint_comm
added
theorem
equiv.perm.disjoint_mul_comm
added
theorem
equiv.perm.disjoint_mul_left
added
theorem
equiv.perm.disjoint_mul_right
added
theorem
equiv.perm.disjoint_one_left
added
theorem
equiv.perm.disjoint_one_right
added
theorem
equiv.perm.disjoint_prod_perm
added
theorem
equiv.perm.disjoint_prod_right
added
theorem
equiv.perm.exists_gpow_eq_of_is_cycle
deleted
theorem
equiv.perm.exists_int_pow_eq_of_is_cycle
added
theorem
equiv.perm.gpow_apply_eq_of_apply_apply_eq_self
added
theorem
equiv.perm.gpow_apply_eq_self_of_apply_eq_self
modified
def
equiv.perm.is_cycle
modified
theorem
equiv.perm.is_cycle_inv
added
theorem
equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self
added
theorem
equiv.perm.of_subtype_one
added
theorem
equiv.perm.pow_apply_eq_of_apply_apply_eq_self
deleted
theorem
equiv.perm.pow_apply_eq_of_apply_apply_eq_self_int
deleted
theorem
equiv.perm.pow_apply_eq_of_apply_apply_eq_self_nat
added
theorem
equiv.perm.pow_apply_eq_self_of_apply_eq_self
added
theorem
equiv.perm.subtype_perm_one
deleted
theorem
equiv.perm.support_swap_mul
deleted
theorem
equiv.perm.support_swap_mul_cycle
added
theorem
equiv.perm.support_swap_mul_eq
added
theorem
equiv.perm.swap_induction_on
Modified
src/linear_algebra/determinant.lean
Modified
test/fin_cases.lean