Theorem RingHom.HoldsForLocalizationAway.containsIdentities

Modification history

2024-09-24 15:04

Mathlib/RingTheory/LocalProperties.lean

chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (#16879) …

Modified RingHom.HoldsForLocalizationAway.containsIdentities View on Github →

2024-09-19 10:59

Mathlib/RingTheory/LocalProperties.lean

chore(AlgebraicGeometry): weaken assumptions on local ring hom properties (#16897) …

Added RingHom.HoldsForLocalizationAway.containsIdentities View on Github →