inv_pair₂ — Mathlib

English

There is a RingHomInvPair between the symmetric Frobenius and its inverse in the opposite direction.

Русский

Существует пара RingHomInvPair между симметричным Фробениусом и его обратным в противоположном направлении.

LaTeX

$$$\text{There is a RingHomInvPair } ((FractionRing.frobenius p k).symm) \; (FractionRing.frobenius p k).$$$

Lean4

instance inv_pair₂ :
    RingHomInvPair ((FractionRing.frobenius p k).symm : K(p, k) →+* K(p, k)) (FractionRing.frobenius p k) :=
  RingHomInvPair.of_ringEquiv (FractionRing.frobenius p k).symm

Похожие утверждения