Theorems · Theorem · ring theory

RingHomInvPair.of_ringEquiv

∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (e : R₁ ≃+* R₂), RingHomInvPair ↑e ↑e.symm

Construct a RingHomInvPair from both directions of a ring equiv. This is not an instance, as for equivalences that are involutions, a better instance would be RingHomInvPair e e.

Defined in

Mathlib.Algebra.Ring.CompTypeclasses

Cited by

15 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

SemiringSemiring