isAdjoinRoot_root_eq_root — Mathlib

English

The root of AdjoinRoot f equals the canonical root: (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f.

Русский

Корень AdjoinRoot f совпадает с каноническим корнем: (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f.

LaTeX

$$$ (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f $$$

Lean4

@[simp]
theorem isAdjoinRoot_root_eq_root : (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f := by
  simp [AdjoinRoot.isAdjoinRoot, IsAdjoinRoot.root]

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