mk_coe' — Mathlib

English

The coercion to Equiv of a ring isomorphism equals the underlying Equiv obtained from it.

Русский

Приведение к эквиваленции кольцевого изоморфизма совпадает с эквивалентностью, полученной из него.

LaTeX

$$$\\operatorname{coe}(f) = f$ as Equiv$$

Lean4

@[simp]
theorem mk_coe' (e : R ≃+* S) (f h₁ h₂ h₃ h₄) : (⟨⟨f, ⇑e, h₁, h₂⟩, h₃, h₄⟩ : S ≃+* R) = e.symm :=
  symm_bijective.injective <| ext fun _ => rfl

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