subalgebraOfSubring — Mathlib

English

A Subring of a ring R gives a Subalgebra of R over the integers, by declaring the ℤ-structure via the usual embedding.

Русский

Подкольцо Subring R образует Subalgebra R над целыми числами, через обычное вложение ℤ → R.

LaTeX

$$$\text{If } S \text{ is a Subring of } R, \quad S \text{ is a Subalgebra } \mathbb{Z} \text{ of } R$$$

Lean4

/-- A subring is a `ℤ`-subalgebra. -/
@[simps toSubsemiring]
def subalgebraOfSubring (S : Subring R) : Subalgebra ℤ R :=
  { S with
    algebraMap_mem' := fun i =>
      Int.induction_on i (by simp) (fun i ih => by simpa using S.add_mem ih S.one_mem) fun i ih =>
        show ((-i - 1 : ℤ) : R) ∈ S by
          rw [Int.cast_sub, Int.cast_one]
          exact S.sub_mem ih S.one_mem }

Похожие утверждения