Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 18:20 12be0aaa

View on Github →

refactor(category_theory/instances): rename examples to instances

Estimated changes

Renamed src/category_theory/examples/measurable_space.lean to src/category_theory/instances/measurable_space.lean

deleted def category_theory.examples.Borel

deleted def category_theory.examples.Meas

added def category_theory.instances.Borel

added def category_theory.instances.Meas

Renamed src/category_theory/examples/monoids.lean to src/category_theory/instances/monoids.lean

deleted def category_theory.examples.CommMon.forget_to_Mon

deleted def category_theory.examples.CommMon

deleted def category_theory.examples.Mon

deleted def category_theory.examples.is_comm_monoid_hom

added def category_theory.instances.CommMon.forget_to_Mon

added def category_theory.instances.CommMon

added def category_theory.instances.Mon

added def category_theory.instances.is_comm_monoid_hom

Renamed src/category_theory/examples/rings.lean to src/category_theory/instances/rings.lean

deleted def category_theory.examples.CommRing.Int.cast

deleted def category_theory.examples.CommRing.Int.hom_unique

deleted def category_theory.examples.CommRing.Int

deleted theorem category_theory.examples.CommRing.comp_val

deleted def category_theory.examples.CommRing.forget

deleted def category_theory.examples.CommRing.forget_to_CommMon

deleted theorem category_theory.examples.CommRing.hom_coe_app

deleted theorem category_theory.examples.CommRing.id_val

deleted def category_theory.examples.CommRing.int.eq_cast'

deleted theorem category_theory.examples.CommRing.polynomial_map_val

deleted theorem category_theory.examples.CommRing.polynomial_obj_α

deleted def category_theory.examples.CommRing.to_Ring

deleted def category_theory.examples.CommRing

deleted def category_theory.examples.Ring

added def category_theory.instances.CommRing.Int.cast

added def category_theory.instances.CommRing.Int.hom_unique

added def category_theory.instances.CommRing.Int

added theorem category_theory.instances.CommRing.comp_val

added def category_theory.instances.CommRing.forget

added def category_theory.instances.CommRing.forget_to_CommMon

added theorem category_theory.instances.CommRing.hom_coe_app

added theorem category_theory.instances.CommRing.id_val

added def category_theory.instances.CommRing.int.eq_cast'

added theorem category_theory.instances.CommRing.polynomial_map_val

added theorem category_theory.instances.CommRing.polynomial_obj_α

added def category_theory.instances.CommRing.to_Ring

added def category_theory.instances.CommRing

added def category_theory.instances.Ring

Renamed src/category_theory/examples/topological_spaces.lean to src/category_theory/instances/topological_spaces.lean

deleted def category_theory.examples.Top.adj₁

deleted def category_theory.examples.Top.adj₂

deleted def category_theory.examples.Top.colimit

deleted def category_theory.examples.Top.colimit_is_colimit

deleted def category_theory.examples.Top.discrete

deleted def category_theory.examples.Top.limit

deleted def category_theory.examples.Top.limit_is_limit

deleted def category_theory.examples.Top.trivial

deleted def category_theory.examples.Top

deleted def category_theory.examples.nbhd

deleted def category_theory.examples.nbhds

added def category_theory.instances.Top.adj₁

added def category_theory.instances.Top.adj₂

added def category_theory.instances.Top.colimit

added def category_theory.instances.Top.colimit_is_colimit

added def category_theory.instances.Top.discrete

added def category_theory.instances.Top.limit

added def category_theory.instances.Top.limit_is_limit

added def category_theory.instances.Top.trivial

added def category_theory.instances.Top

added def category_theory.instances.nbhd

added def category_theory.instances.nbhds