Commit 2023-01-27 05:22 526ab32a

View on Github →

chore: fix casing errors per naming scheme (#1670)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Algebra/CovariantAndContravariant.lean

Modified Mathlib/Algebra/GCDMonoid/Finset.lean

Modified Mathlib/Algebra/GCDMonoid/Multiset.lean

Modified Mathlib/Algebra/Group/Prod.lean

Modified Mathlib/Algebra/Hom/Centroid.lean

added theorem CentroidHom.coe_toAddMonoidHom

added theorem CentroidHom.coe_toAddMonoidHom_injective

deleted theorem CentroidHom.coe_to_add_monoid_hom

deleted theorem CentroidHom.coe_to_add_monoid_hom_injective

added theorem CentroidHom.toAddMonoidHom_eq_coe

deleted theorem CentroidHom.to_add_monoid_hom_eq_coe

Modified Mathlib/Algebra/Hom/Equiv/Units/Basic.lean

Modified Mathlib/Algebra/Module/Basic.lean

added theorem smulAddHom_apply

deleted theorem smul_add_hom_apply

Modified Mathlib/Algebra/Parity.lean

Modified Mathlib/Algebra/Ring/CompTypeclasses.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/FinEnum.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Lattice.lean

Modified Mathlib/Data/Finset/Sigma.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/List/AList.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Card.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/Multiset/FinsetOps.lean

Modified Mathlib/Data/PNat/Prime.lean

Modified Mathlib/Data/PNat/Xgcd.lean

Modified Mathlib/Data/Part.lean

Modified Mathlib/Data/Rat/Cast.lean

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

Modified Mathlib/Data/Set/NAry.lean

Modified Mathlib/Data/Set/Pointwise/Basic.lean

Modified Mathlib/Data/Set/Pointwise/SMul.lean

Modified Mathlib/Data/Sigma/Basic.lean

Modified Mathlib/Data/TypeVec.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

Modified Mathlib/GroupTheory/Subsemigroup/Operations.lean

Modified Mathlib/Init/Logic.lean

added theorem decidableEq_inl_refl

added theorem decidableEq_inr_neg

added def decidableEq_of_bool_pred

deleted theorem decidable_eq_inl_refl

deleted theorem decidable_eq_inr_neg

deleted def decidable_eq_of_bool_pred

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Function/Conjugate.lean

Modified Mathlib/Order/Antichain.lean

Modified Mathlib/Order/Concept.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/Hom/Bounded.lean

added theorem BoundedOrderHom.coe_comp_botHom

deleted theorem BoundedOrderHom.coe_comp_bot_hom

added theorem BoundedOrderHom.coe_comp_orderHom

deleted theorem BoundedOrderHom.coe_comp_order_hom

added theorem BoundedOrderHom.coe_comp_topHom

deleted theorem BoundedOrderHom.coe_comp_top_hom

Modified Mathlib/Order/ModularLattice.lean

Modified Mathlib/Order/Monotone/Monovary.lean

Modified Mathlib/Order/Monotone/Odd.lean

added theorem antitone_of_odd_of_monotoneOn_nonneg

deleted theorem antitone_of_odd_of_monotone_on_nonneg

added theorem monotone_of_odd_of_monotoneOn_nonneg

deleted theorem monotone_of_odd_of_monotone_on_nonneg

added theorem strictAnti_of_odd_strictAntiOn_nonneg

deleted theorem strictAnti_of_odd_strictAnti_on_nonneg

added theorem strictMono_of_odd_strictMonoOn_nonneg

deleted theorem strictMono_of_odd_strictMono_on_nonneg

Modified Mathlib/Order/SemiconjSup.lean

Modified Mathlib/Order/Zorn.lean

Modified Mathlib/RingTheory/Congruence.lean

Modified Mathlib/Tactic/ApplyFun.lean

Modified scripts/nolints.json