equivOfRoot_map — Mathlib

English

For pb : PowerBasis A S and e : S ≃ₐ[A] S', we have pb.equivOfRoot pb' h₁ h₂ (where pb' = pb.map e) equals e; i.e., pb.equivOfRoot (pb.map e) h₁ h₂ = e.

Русский

Для pb : PowerBasis A S и e : S ≃ₐ[A] S', имеет место pb.equivOfRoot pb' h₁ h₂ (где pb' = pb.map e) равное e.

LaTeX

$$$ pb.equivOfRoot (pb.map e) h_1 h_2 = e $$$

Lean4

@[simp]
theorem equivOfRoot_map (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ h₂) : pb.equivOfRoot (pb.map e) h₁ h₂ = e :=
  by
  ext x
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  simp [aeval_algEquiv]

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