adjoinRootXPowSubCEquiv_symm_eq_root

English

The symmetry of adjoinRootXPowSubCEquiv yields equality of the inverse action on the root with the canonical root.

Русский

Симметрия adjoinRootXPowSubCEquiv даёт равенство обратного действия на корень с каноническим корнем.

LaTeX

$$$adjoinRootXPowSubCEquiv\\; hζ\\; H\\; hα\\; (root) = root$$$

Lean4

theorem adjoinRootXPowSubCEquiv_symm_eq_root : (adjoinRootXPowSubCEquiv hζ H hα).symm α = root _ :=
  by
  apply (adjoinRootXPowSubCEquiv hζ H hα).injective
  rw [(adjoinRootXPowSubCEquiv hζ H hα).apply_symm_apply, adjoinRootXPowSubCEquiv_root]

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