Commit 2025-08-21 13:56 31fb1c4a

View on Github →

chore(*): address some @[simps] porting notes (#28517) Search for porting notes mentioning simps and fix the ones that are easy to fix. The search also caught some that refer to simps as in a simp set, so we fix them too.

Estimated changes

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

deleted theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit

deleted theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit

added theorem AlgebraicGeometry.ΓSpec.toSpecΓ_of

added theorem AlgebraicGeometry.ΓSpec.toSpecΓ_unop

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

Modified Mathlib/CategoryTheory/Monad/Adjunction.lean

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

Modified Mathlib/CategoryTheory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

deleted theorem LinearIndependent.linearCombinationEquiv_apply_coe

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

Modified Mathlib/RepresentationTheory/Rep.lean

deleted theorem Rep.homEquiv_apply_hom

deleted theorem Rep.homEquiv_symm_apply_hom

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean