Commit 2023-01-07 14:35 0ee6552e

View on Github →

chore: tidy various files (#1412)

Estimated changes

Modified Mathlib/Algebra/Associated.lean

added theorem Associates.mkMonoidHom_apply

deleted theorem Associates.mk_monoidHom_apply

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

modified def associatesEquivOfUniqueUnits

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

added theorem WithBot.coe_bit0

added theorem WithBot.coe_bit1

added theorem WithTop.coe_bit0

added theorem WithTop.coe_bit1

Modified Mathlib/Algebra/Tropical/Basic.lean

added theorem Tropical.leftInverse_trop

deleted theorem Tropical.left_inverse_trop

added theorem Tropical.rightInverse_trop

deleted theorem Tropical.right_inverse_trop

added theorem Tropical.tropOrderIso_coe_fn

added theorem Tropical.tropOrderIso_symm_coe_fn

deleted theorem Tropical.trop_order_iso_coe_fn

deleted theorem Tropical.trop_order_iso_symm_coe_fn

Modified Mathlib/Data/Bool/AllAny.lean

Modified Mathlib/Data/List/Infix.lean

Modified Mathlib/Data/Set/Intervals/OrdConnectedComponent.lean

added theorem Set.mem_ordConnectedComponent_ordConnectedProj

deleted theorem Set.mem_ordConnectedComponent_ord_connected_proj

added theorem Set.ordConnectedComponent_ordConnectedProj

deleted theorem Set.ordConnectedComponent_ord_connected_proj

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

modified def Equiv.toLocalEquiv

added theorem Equiv.transLocalEquiv_eq_trans

deleted theorem Equiv.trans_localEquiv_eq_trans

added theorem LocalEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn

deleted theorem LocalEquiv.IsImage.inter_eq_of_inter_eq_of_eq_on

modified def LocalEquiv.IsImage.restr

added theorem LocalEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn

deleted theorem LocalEquiv.IsImage.symm_eq_on_of_inter_eq_of_eq_on

added theorem LocalEquiv.disjointUnion_eq_piecewise

deleted theorem LocalEquiv.disjoint_union_eq_piecewise

modified def LocalEquiv.prod

Modified Mathlib/Order/Concept.lean

added theorem Concept.strictAnti_snd

added theorem Concept.strictMono_fst

deleted theorem Concept.strict_anti_snd

deleted theorem Concept.strict_mono_fst

modified def Concept.swapEquiv

added theorem extentClosure_Union₂

added theorem extentClosure_anti

added theorem extentClosure_empty

added theorem extentClosure_intentClosure_extentClosure

added theorem extentClosure_swap

added theorem extentClosure_union

added theorem extentClosure_unionᵢ

deleted theorem extent_closure_Union₂

deleted theorem extent_closure_anti

deleted theorem extent_closure_empty

deleted theorem extent_closure_intent_closure_extent_closure

deleted theorem extent_closure_swap

deleted theorem extent_closure_union

deleted theorem extent_closure_unionᵢ

added theorem gc_intentClosure_extentClosure

deleted theorem gc_intent_closure_extent_closure

added theorem intentClosure_anti

added theorem intentClosure_empty

added theorem intentClosure_extentClosure_intentClosure

added theorem intentClosure_swap

added theorem intentClosure_union

added theorem intentClosure_unionᵢ

added theorem intentClosure_unionᵢ₂

deleted theorem intent_closure_anti

deleted theorem intent_closure_empty

deleted theorem intent_closure_extent_closure_intent_closure

deleted theorem intent_closure_swap

deleted theorem intent_closure_union

deleted theorem intent_closure_unionᵢ

deleted theorem intent_closure_unionᵢ₂

added theorem subset_extentClosure_intentClosure

deleted theorem subset_extent_closure_intent_closure

added theorem subset_intentClosure_extentClosure

added theorem subset_intentClosure_iff_subset_extentClosure

deleted theorem subset_intent_closure_extent_closure

deleted theorem subset_intent_closure_iff_subset_extent_closure

Modified Mathlib/Order/Extension/Linear.lean

added theorem extend_partialOrder

deleted theorem extend_partial_order