Theorem NonUnitalSubsemiring.mem_map

Modification history

2026-09-10 16:50
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
refactor: make several definitions take concrete morphism classes (#43596) …
Modified NonUnitalSubsemiring.mem_mapView on Github →
2024-04-08 10:17
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
chore: remove more `bex` and `ball` from lemma names (#11615) …
Modified NonUnitalSubsemiring.mem_mapView on Github →
2023-04-14 23:46
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
feat: Port `RingTheory.NonUnitalSubsemiring.Basic` (#1774)
Added NonUnitalSubsemiring.mem_mapView on Github →