Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-20 15:51 9822b65b

View on Github →

chore(*): add missing coe_copy and copy_eq (#17615)

Estimated changes

added theorem centroid_hom.coe_copy
added theorem centroid_hom.copy_eq
added theorem monoid_hom.coe_copy
added theorem monoid_hom.copy_eq
added theorem mul_hom.coe_copy
added theorem mul_hom.coe_copy_eq
added theorem one_hom.coe_copy
added theorem one_hom.coe_copy_eq
added theorem ring_hom.coe_copy
added theorem ring_hom.copy_eq
added theorem linear_map.coe_copy
added theorem linear_map.copy_eq
added theorem order_ring_hom.copy_eq
added theorem star_alg_hom.coe_copy
added theorem star_alg_hom.copy_eq
added theorem ssyt.coe_copy
added theorem ssyt.copy_eq
added theorem quadratic_form.copy_eq
added theorem local_equiv.copy_eq
deleted theorem local_equiv.copy_eq_self
added theorem biheyting_hom.coe_copy
added theorem biheyting_hom.copy_eq
added theorem coheyting_hom.coe_copy
added theorem coheyting_hom.copy_eq
added theorem heyting_hom.coe_copy
added theorem heyting_hom.copy_eq
added theorem order_hom.coe_copy
added theorem order_hom.copy_eq
added theorem bot_hom.coe_copy
added theorem bot_hom.copy_eq
added theorem top_hom.coe_copy
added theorem top_hom.copy_eq
added theorem Inf_hom.coe_copy
added theorem Inf_hom.copy_eq
added theorem Sup_hom.coe_copy
added theorem Sup_hom.copy_eq
added theorem frame_hom.coe_copy
added theorem frame_hom.copy_eq
added theorem inf_hom.coe_copy
added theorem inf_hom.copy_eq
added theorem inf_top_hom.coe_copy
added theorem inf_top_hom.copy_eq
added theorem lattice_hom.coe_copy
added theorem lattice_hom.copy_eq
added theorem sup_bot_hom.coe_copy
added theorem sup_bot_hom.copy_eq
added theorem sup_hom.coe_copy
added theorem sup_hom.copy_eq
added theorem continuous_map.copy_eq
added theorem cocompact_map.coe_copy
added theorem cocompact_map.copy_eq
added theorem esakia_hom.coe_copy
added theorem esakia_hom.copy_eq
added theorem spectral_map.coe_copy
added theorem spectral_map.copy_eq