Characteristic of the order type synonyms

Transfer characteristic instances from R to Rᵒᵈ and Lex R.

Order dual

instance OrderDual.instCharZero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] : CharZero Rᵒᵈ

instance OrderDual.instCharP {R : Type u_1} {p : ℕ} [AddMonoidWithOne R] [CharP R p] : CharP Rᵒᵈ p

instance OrderDual.instExpChar {R : Type u_1} {p : ℕ} [AddMonoidWithOne R] [ExpChar R p] : ExpChar Rᵒᵈ p

@[simp]

theorem OrderDual.ringChar_eq {R : Type u_1} [NonAssocSemiring R] : ringChar Rᵒᵈ = ringChar R

Lexicographical order

instance Lex.instCharZero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] : CharZero (Lex R)

instance Lex.instCharP {R : Type u_1} {p : ℕ} [AddMonoidWithOne R] [CharP R p] : CharP (Lex R) p

instance Lex.instExpChar {R : Type u_1} {p : ℕ} [AddMonoidWithOne R] [ExpChar R p] : ExpChar (Lex R) p

@[simp]

theorem Lex.ringChar_eq {R : Type u_1} [NonAssocSemiring R] : ringChar (Lex R) = ringChar R