# mathlibdocumentation

algebra.char_p.algebra

# Characteristics of algebras #

In this file we describe the characteristic of R-algebras.

In particular we are interested in the characteristic of free algebras over R and the fraction field fraction_ring R.

## Main results #

• char_p_of_injective_algebra_map If R →+* A is an injective algebra map then A has the same characteristic as R.

Instances constructed from this result:

• Any free_algebra R X has the same characteristic as R.
• The fraction_ring R of an integral domain R has the same characteristic as R.
theorem char_p_of_injective_algebra_map {R : Type u_1} {A : Type u_2} [semiring A] [ A] (h : function.injective A)) (p : ) [ p] :
p

If the algebra map R →+* A is injective then A has the same characteristic as R.

theorem char_zero_of_injective_algebra_map {R : Type u_1} {A : Type u_2} [semiring A] [ A] (h : function.injective A)) [char_zero R] :

If the algebra map R →+* A is injective and R has characteristic zero then so does A.

theorem algebra.char_p_iff (K : Type u_1) (L : Type u_2) [field K] [nontrivial L] [ L] (p : ) :
p p
@[instance]
def free_algebra.char_p {R : Type u_1} {X : Type u_2} (p : ) [ p] :
char_p X) p

If R has characteristic p, then so does free_algebra R X.

@[instance]
def free_algebra.char_zero {R : Type u_1} {X : Type u_2} [char_zero R] :

If R has characteristic 0, then so does free_algebra R X.

theorem is_fraction_ring.char_p_of_is_fraction_ring (R : Type u_1) {K : Type u_2} [field K] [ K] [ K] (p : ) [ p] :
p

If R has characteristic p, then so does Frac(R).

@[instance]
def is_fraction_ring.char_p (R : Type u_1) (p : ) [ p] :
p

If R has characteristic p, then so does fraction_ring R.

theorem is_fraction_ring.char_zero_of_is_fraction_ring (R : Type u_1) {K : Type u_2} [field K] [ K] [ K] [char_zero R] :

If R has characteristic 0, then so does Frac(R).

@[instance]
def is_fraction_ring.char_zero (R : Type u_1) [char_zero R] :

If R has characteristic 0, then so does fraction_ring R.