Commit 2023-02-07 20:20 3d72b547

View on Github →

feat: port Topology.LocallyConstant.Basic (#2141)

Estimated changes

added theorem IsLocallyConstant.desc
added theorem IsLocallyConstant.div
added theorem IsLocallyConstant.inv
added theorem IsLocallyConstant.mul
added theorem IsLocallyConstant.one
added theorem LocallyConstant.coe_mk
added theorem LocallyConstant.ext
added theorem LocallyConstant.map_id
added structure LocallyConstant