rangeRestrictFieldEquiv_apply_symm_apply

English

For any f, the rangeRestrictFieldEquiv satisfies f(rangeRestrictFieldEquiv^{-1}(x)) = x for x in f.fieldRange.

Русский

Для любого f выполняется f( rangeRestrictFieldEquiv^{-1}(x) ) = x для x из f.fieldRange.

LaTeX

$$$f\big( f.rangeRestrictFieldEquiv^{-1}(x) \big) = x$$$

Lean4

@[simp]
theorem rangeRestrictFieldEquiv_apply_symm_apply (f : K →+* L) (x : f.fieldRange) :
    f (f.rangeRestrictFieldEquiv.symm x) = x := by rw [← rangeRestrictFieldEquiv_apply_coe, RingEquiv.apply_symm_apply]

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