Theorems · Definition · commutative algebra
Subring.toAddSubgroup
{R : Type u} → [inst : NonAssocRing R] → Subring R → AddSubgroup RReinterpret a Subring as an AddSubgroup.
- Defined in
- Mathlib.Algebra.Ring.Subring.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- NonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddSubgroupstatement · cited by 3,232
- Subringstatement and proof · cited by 602
- NonAssocRingstatement and proof · cited by 483
- Subsemigroup.carrierproof · cited by 160
- Submonoid.toSubsemigroupproof · cited by 159
- Subsemiring.toSubmonoidproof · cited by 153
- Subring.toSubsemiringproof · cited by 71
- Subring.neg_mem'proof · cited by 1
- Subsemiring.add_mem'proof · cited by 0
- Subsemiring.zero_mem'proof · cited by 0
Cited by20
Results whose statement or proof uses this declaration.
- Subring.mapproof · cited by 33
- Subring.subtypeproof · cited by 22
- Subring.comapproof · cited by 22
- Subring.prodproof · cited by 11
- Valuation.leIdealproof · cited by 7
- Valuation.ltIdealproof · cited by 4
- Subring.topologicalClosureproof · cited by 4
- Subring.mem_iSup_of_directedproof · cited by 3
- Subfield.toAddSubgroupproof · cited by 2
- Subring.mk'_toAddSubgroupstatement and proof · cited by 1
- Subring.toAddSubgroup_strictMonostatement · cited by 1
- Subring.pointwise_smul_toAddSubgroupstatement · cited by 0