Theorem NonUnitalSubsemiring.comap_center_le_center

Modification history

2026-09-10 16:50
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
refactor: make several definitions take concrete morphism classes (#43596) …
Modified NonUnitalSubsemiring.comap_center_le_centerView on Github →
2026-08-18 12:48
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
feat(Algebra): `center` map lemmas (#42105) …
Added NonUnitalSubsemiring.comap_center_le_centerView on Github →