Commit 2024-07-24 23:20 aa84124d

View on Github →

chore: protect congr_arg's and congr_fun's (#15083) We already have congr_arg and congr_fun in the root namespace.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/EpiMono.lean

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

Modified Mathlib/Algebra/Polynomial/DenomsClearable.lean

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

deleted theorem RingHom.congr_arg

deleted theorem RingHom.congr_fun

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/GroupTheory/Transfer.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

deleted theorem AlternatingMap.congr_arg

deleted theorem AlternatingMap.congr_fun

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

deleted theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg

deleted theorem OmegaCompletePartialOrder.ContinuousHom.congr_fun

Modified Mathlib/Topology/Homotopy/Basic.lean

deleted theorem ContinuousMap.Homotopy.congr_arg

deleted theorem ContinuousMap.Homotopy.congr_fun

Modified Mathlib/Topology/LocallyConstant/Basic.lean

deleted theorem LocallyConstant.congr_arg

deleted theorem LocallyConstant.congr_fun

Modified Mathlib/Topology/MetricSpace/Dilation.lean

deleted theorem Dilation.congr_arg

deleted theorem Dilation.congr_fun