Theorem Subring.toAddSubgroup_strictMono

Modification history

2023-02-11 16:08

Mathlib/RingTheory/Subring/Basic.lean

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

Added Subring.toAddSubgroup_strictMono View on Github →