Theorems · Inductive type · ring theory

RingHomInvPair

{R₁ : Type u_1} →
  {R₂ : Type u_2} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → (R₁ →+* R₂) → outParam (R₂ →+* R₁) → Prop

Class that expresses the fact that two ring homomorphisms are inverses of each other. This is used to handle symm for semilinear equivalences.

Defined in: Mathlib.Algebra.Ring.CompTypeclasses
Cited by: 523 results in Mathlib
Foundations: Depth 11 from the axioms, rests on 81 definitions · uses no axioms
Assumes: Semiring Semiring

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 632.