Commit 2023-06-14 02:21 fa225598

View on Github →

chore: forward-port leanprover-community/mathlib#15681 (complete) (#4939) Removed diagonal stuff which is no longer needed.

Estimated changes

modified def Cube.boundary
deleted theorem Cube.boundary_one
deleted theorem Cube.boundary_zero
deleted theorem Cube.head.continuous
deleted def Cube.head
added def Cube.insertAt
added theorem Cube.insertAt_boundary
deleted theorem Cube.mem_boundary
deleted theorem Cube.one_char
deleted theorem Cube.one_mem_boundary
deleted theorem Cube.proj_continuous
added def Cube.splitAt
deleted def Cube.tail
deleted theorem Cube.zero_mem_boundary
deleted def Cube
modified theorem GenLoop.Homotopic.equiv
modified theorem GenLoop.Homotopic.refl
modified def GenLoop.Homotopic
added theorem GenLoop.boundary
added theorem GenLoop.coe_copy
modified def GenLoop.const
added theorem GenLoop.const_apply
added def GenLoop.copy
added theorem GenLoop.copy_eq
deleted def GenLoop.diagonal
modified theorem GenLoop.ext
added def GenLoop.fromLoop
added theorem GenLoop.fromLoop_apply
added theorem GenLoop.homotopicFrom
added theorem GenLoop.homotopicTo
modified theorem GenLoop.mk_apply
added def GenLoop.symmAt
added def GenLoop.toLoop
added theorem GenLoop.toLoop_apply
added theorem GenLoop.to_from
added def GenLoop.transAt
added def GenLoop
deleted structure GenLoop
added def HomotopyGroup.Pi
added theorem HomotopyGroup.inv_spec
added theorem HomotopyGroup.mul_spec
added theorem HomotopyGroup.one_def
modified def HomotopyGroup
added def LoopSpace
deleted def genLoopZeroEquiv