isDomain — Mathlib

English

Let e: α ≃ β with Semiring β and IsDomain β. Then α inherits IsDomain via transported semiring structure along e.

Русский

Пусть e: α ≃ β; β—семиринг и находится IsDomain β. Тогда α наследует свойство IsDomain через перенос структуры вдоль e.

LaTeX

$$$IsDomain(α)\; \text{ given } e:\ α\simeq β, β \text{ is a Semiring and IsDomain}(β)$$$

Lean4

/-- Transfer `IsDomain` across an `Equiv` -/
protected theorem isDomain [Semiring β] [IsDomain β] (e : α ≃ β) :
    letI := e.semiring
    IsDomain α :=
  letI := e.semiring;
  e.injective.isDomain e.ringEquiv

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