Commit 2026-01-23 14:21 3cfe4334

View on Github →

chore: add missing mem lemmas (#33801)

Add missing simp lemmas mem_foo where a simp lemma coe_foo already exists

Estimated changes

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.mem_opensRange

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

modified theorem FractionalIdeal.coe_mem_one

Modified Mathlib/RingTheory/FractionalIdeal/Extended.lean

Modified Mathlib/Topology/Category/TopCat/Opens.lean

added theorem TopologicalSpace.Opens.mem_map

Modified Mathlib/Topology/Sets/Opens.lean

added theorem TopologicalSpace.Opens.mem_sup