Theorems · Definition · ring theory

Algebra.linearMap

(R : Type u) → (A : Type w) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → R →ₗ[R] A

The canonical ring homomorphism algebraMap R A : R →+* A for any R-algebra A, packaged as an R-linear map.

Defined in

Mathlib.Algebra.Algebra.Defs

Cited by

157 results in Mathlib

Foundations

Depth 20 from the axioms, rests on 193 definitions · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra