isField — Mathlib

English

A is a field if B is a field and A is isomorphic to B via a multiplicative equivalence.

Русский

Если B является полем и A изоморфно B посредством мультипликативного эквивалента, то A — поле.

LaTeX

$$$\text{If } e: A \simeq^* B ext{ and } B ext{ is a field, then } A ext{ is a field.}$$$

Lean4

protected theorem isField (hB : IsField B) (e : A ≃* B) : IsField A :=
  IsLocalHom.isField e.injective hB

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