congr_apply — Mathlib

English

For any x in A ⊗_R B, the action of congr f g on x agrees with the canonical map obtained by applying f on A and g on B.

Русский

Для любого x ∈ A ⊗_R B конгруэнция f,g действует на x так же, как и канонический отображение, получаемый применением f к A и g к B.

LaTeX

$$congr(f,g)(x) = map(f,g)(x)$$

Lean4

@[simp]
theorem congr_apply (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x) : congr f g x = (map (f : A →ₐ[S] C) (g : B →ₐ[R] D)) x :=
  rfl

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