Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-05 06:26 4c3e1721

View on Github →

feat(topology/homotopy/homotopy_group): group and comm_group instances for π_n (#15681) This PR adds:

  • Group instance for π_(n+1)
  • Commutative group instance for π_(n+2)

Estimated changes

modified def cube.boundary
deleted theorem cube.head.continuous
deleted def cube.head
added def cube.insert_at
deleted theorem cube.one_char
deleted theorem cube.proj_continuous
added def cube.split_at
deleted def cube.tail
deleted def cube
added theorem gen_loop.boundary
added theorem gen_loop.coe_copy
modified def gen_loop.const
added theorem gen_loop.const_apply
added def gen_loop.copy
added theorem gen_loop.copy_eq
modified theorem gen_loop.ext
modified theorem gen_loop.homotopic.equiv
modified theorem gen_loop.homotopic.refl
modified theorem gen_loop.homotopic.symm
modified theorem gen_loop.homotopic.trans
modified def gen_loop.homotopic
added theorem gen_loop.homotopic_to
modified theorem gen_loop.mk_apply
added def gen_loop.symm_at
added theorem gen_loop.to_from
added def gen_loop.to_loop
added theorem gen_loop.to_loop_apply
added def gen_loop
deleted structure gen_loop
deleted def gen_loop_zero_equiv
added theorem homotopy_group.one_def
modified def homotopy_group
added def loop_space