Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-16 20:09 910de7ec

View on Github →

refactor(group_theory/coset): left_cosets is now a quotient (#103)

Estimated changes

Modified data/equiv.lean

added def equiv.equiv_fib

Modified group_theory/coset.lean

deleted theorem is_subgroup.Union_left_cosets_eq_univ

deleted theorem is_subgroup.group_equiv_left_cosets_times_subgroup

added def is_subgroup.left_coset_equiv_subgroup

deleted theorem is_subgroup.left_cosets_disjoint

deleted theorem is_subgroup.left_cosets_equiv_subgroup

deleted theorem is_subgroup.pairwise_left_cosets_disjoint

deleted theorem is_subgroup.subgroup_mem_left_cosets

added def left_cosets.left_coset

modified def left_cosets

Modified group_theory/order_of_element.lean