Commit 2022-12-17 23:54 4e2a7237

View on Github →

chore: tidy various files (#1086)

Estimated changes

added theorem ofDual_rat_cast
added theorem ofLex_rat_cast
deleted theorem of_dual_rat_cast
deleted theorem of_lex_rat_cast
added theorem toDual_rat_cast
added theorem toLex_rat_cast
deleted theorem to_dual_rat_cast
deleted theorem to_lex_rat_cast
added theorem Units.coe_opEquiv_symm
deleted theorem Units.coe_op_equiv_symm
added theorem Units.coe_unop_opEquiv
deleted theorem Units.coe_unop_op_equiv
deleted theorem RingHom.coe_monoid_hom_id
added theorem RingHom.isUnit_map
deleted theorem RingHom.is_unit_map
added theorem strictAnti_iff_map_neg
added theorem strictAnti_iff_map_pos
added theorem strictMono_iff_map_neg
added theorem strictMono_iff_map_pos
deleted theorem strict_anti_iff_map_neg
deleted theorem strict_anti_iff_map_pos
deleted theorem strict_mono_iff_map_neg
deleted theorem strict_mono_iff_map_pos
added theorem Bool.ofNat_le_ofNat
added theorem Bool.ofNat_toNat
deleted theorem Bool.of_nat_le_of_nat
deleted theorem Bool.of_nat_to_nat
added theorem Bool.toNat_le_toNat
deleted theorem Bool.to_nat_le_to_nat
added theorem Int.castAddHom_int
added theorem Int.castRingHom_int
deleted theorem Int.cast_add_hom_int
deleted theorem Int.cast_ring_hom_int
added theorem Int.cast_strictMono
deleted theorem Int.cast_strict_mono
added theorem Int.coe_castAddHom
added theorem Int.coe_castRingHom
deleted theorem Int.coe_cast_add_hom
deleted theorem Int.coe_cast_ring_hom
added theorem ofDual_int_cast
added theorem ofLex_int_cast
deleted theorem of_dual_int_cast
deleted theorem of_lex_int_cast
added theorem toDual_int_cast
added theorem toLex_int_cast
deleted theorem to_dual_int_cast
deleted theorem to_lex_int_cast
modified theorem Int.exists_greatest_of_bdd
modified theorem Int.exists_least_of_bdd
added theorem Int.lt_of_toNat_lt
deleted theorem Int.lt_of_to_nat_lt
added theorem Int.lt_toNat
deleted theorem Int.lt_to_nat
added theorem Int.toNat_eq_zero
added theorem Int.toNat_le
added theorem Int.toNat_le_toNat
added theorem Int.toNat_lt_toNat
added theorem Int.toNat_sub_of_le
deleted theorem Int.to_nat_eq_zero
deleted theorem Int.to_nat_le
deleted theorem Int.to_nat_le_to_nat
deleted theorem Int.to_nat_lt_to_nat
deleted theorem Int.to_nat_sub_of_le
added theorem NeZero.nat_of_neZero
deleted theorem NeZero.nat_of_ne_zero
deleted theorem Nat.pow_left_strict_mono
deleted theorem Nat.pow_right_strict_mono
added theorem PEquiv.isSome_symm_get
deleted theorem PEquiv.is_some_symm_get
added theorem Set.preimage_setOf_eq
deleted theorem Set.preimage_set_of_eq
deleted theorem Set.proj_Icc_of_right_le
added theorem Vector.toList_append
added theorem Vector.toList_cons
added theorem Vector.toList_drop
added theorem Vector.toList_length
added theorem Vector.toList_nil
added theorem Vector.toList_take
deleted theorem Vector.to_list_append
deleted theorem Vector.to_list_cons
deleted theorem Vector.to_list_drop
deleted theorem Vector.to_list_length
deleted theorem Vector.to_list_nil
deleted theorem Vector.to_list_take
added theorem isGLB_Icc
added theorem isGLB_Ico
added theorem isGLB_Ioc
added theorem isGLB_Ioo
added theorem isGLB_univ
deleted theorem is_glb_Icc
deleted theorem is_glb_Ico
deleted theorem is_glb_Ioc
deleted theorem is_glb_Ioo
deleted theorem is_glb_univ
added theorem directedOn_image
added theorem directedOn_of_inf_mem
deleted theorem directed_on_image
deleted theorem directed_on_of_inf_mem
added theorem isDirected_mono
deleted theorem is_directed_mono
added theorem InitialSeg.leLt_apply
deleted theorem InitialSeg.le_lt_apply
deleted theorem PrincipalSeg.equiv_lt_top