Theorems · Definition · ring theory

SetLike.GradeZero.subalgebra

{ι : Type u_1} →
  {S : Type u_3} →
    {R : Type u_4} →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : Algebra S R] →
            [inst_3 : AddMonoid ι] → (A : ι → Submodule S R) → [SetLike.GradedMonoid A] → Subalgebra S R

The subalgebra A 0 of R.

Defined in: Mathlib.Algebra.DirectSum.Internal
Cited by: 0 results in Mathlib
Foundations: Depth 21 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring Semiring Algebra AddMonoid SetLike.GradedMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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
Submodulestatement and proof · cited by 7,192
AddMonoidstatement and proof · cited by 2,864
Subalgebrastatement · cited by 1,353
Subsemiringproof · cited by 456
SetLike.GradedMonoidstatement and proof · cited by 48
SetLike.GradeZero.subsemiringproof · cited by 0

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.