Theorems · Definition · ring theory

Subalgebra.toAddSubmonoid

{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A → AddSubmonoid A

The projection from a subalgebra of A to an additive submonoid of A.

Defined in: Mathlib.Algebra.Algebra.Subalgebra.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 13 from the axioms · uses no axioms
Assumes: CommSemiring Semiring Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
Subalgebrastatement and proof · cited by 1,353
AddSubmonoidstatement · cited by 1,178
Subalgebra.toSubsemiringproof · cited by 115
Subsemiring.toAddSubmonoidproof · cited by 20

Cited by2

Results whose statement or proof uses this declaration.

Algebra.FinitePresentation.ker_fg_of_mvPolynomialproof · cited by 1
AlgHom.subalgebraMap_surjectiveproof · cited by 0