Theorems · Theorem · commutative algebra

RingCon.coe_algebraMap

∀ {α : Type u_1} {R : Type u_3} [inst : CommSemiring α] [inst_1 : Semiring R] [inst_2 : Algebra α R] (c : RingCon R)
  (s : α), ↑((algebraMap α R) s) = (algebraMap α c.Quotient) s

Defined in

Mathlib.RingTheory.Congruence.Basic

Cited by

1 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra