mathlib3 documentation


Ring involutions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines a ring involution as a structure extending R ≃+* Rᵐᵒᵖ, with the additional fact f.involution : (f (f x).unop).unop = x.

Notations #

We provide a coercion to a function R → Rᵐᵒᵖ.

References #

Tags #

Ring involution

structure ring_invo (R : Type u_1) [semiring R] :
Type u_1

A ring involution

Instances for ring_invo
def ring_invo.to_ring_equiv {R : Type u_1} [semiring R] (self : ring_invo R) :

The equivalence of rings underlying a ring involution.

structure ring_invo_class (F : Type u_2) (R : out_param (Type u_3)) [semiring R] :
Type (max u_2 u_3)

ring_invo_class F R S states that F is a type of ring involutions. You should extend this class when you extend ring_invo.

Instances of this typeclass
Instances of other typeclasses for ring_invo_class
  • ring_invo_class.has_sizeof_inst
@[protected, instance]
def' {R : Type u_1} [semiring R] (f : R →+* Rᵐᵒᵖ) (involution : (r : R), mul_opposite.unop (f (mul_opposite.unop (f r))) = r) :

Construct a ring involution from a ring homomorphism.

@[protected, instance]

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

theorem ring_invo.to_fun_eq_coe {R : Type u_1} [semiring R] (f : ring_invo R) :
theorem ring_invo.involution {R : Type u_1} [semiring R] (f : ring_invo R) (x : R) :
theorem ring_invo.coe_ring_equiv {R : Type u_1} [semiring R] (f : ring_invo R) (a : R) :
f a = f a
theorem ring_invo.map_eq_zero_iff {R : Type u_1} [semiring R] (f : ring_invo R) {x : R} :
f x = 0 x = 0
def (R : Type u_1) [comm_ring R] :

The identity function of a comm_ring is a ring involution.

@[protected, instance]