Commit 2025-03-03 19:22 1200a068

View on Github →

chore: fix some underscores in names (#19909) There's lots where this came from: search for _is_ to find lots of incorrectly named statements.

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.isLocalization_basicOpen_of_qcqs

deleted theorem AlgebraicGeometry.is_localization_basicOpen_of_qcqs

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/RingTheory/Localization/LocalizationLocalization.lean

Modified Mathlib/RingTheory/RingHom/FiniteType.lean

added theorem RingHom.finiteType_isLocal

deleted theorem RingHom.finiteType_is_local

Modified Mathlib/RingTheory/RingHomProperties.lean

added theorem RingHom.RespectsIso.isLocalization_away_iff

deleted theorem RingHom.RespectsIso.is_localization_away_iff

Modified scripts/nolints_prime_decls.txt