Theorem Subring.coeSubtype

Modification history

2024-11-05 11:39

Mathlib/Algebra/Ring/Subring/Basic.lean

chore(Algebra/Ring/Subring): split `Basic.lean` (#18520) …

Modified Subring.coeSubtype View on Github →

2023-02-11 16:08

Mathlib/RingTheory/Subring/Basic.lean

feat: port RingTheory.Subring.Basic (#1945)

Added Subring.coeSubtype View on Github →