restriction — Mathlib

English

The restriction of a power-multiplicative function to a subalgebra is again power-multiplicative.

Русский

Ограничение функции, сохраняющей степень, на подалгебру снова сохраняет это свойство.

LaTeX

$$$\text{Restriction of IsPowMul to } A \text{ is IsPowMul}$$$

Lean4

/-- The restriction of a power-multiplicative function to a subalgebra is power-multiplicative. -/
theorem restriction {R S : Type*} [CommRing R] [Ring S] [Algebra R S] (A : Subalgebra R S) {f : S → ℝ}
    (hf_pm : IsPowMul f) : IsPowMul fun x : A => f x.val := fun x n hn => by simpa using hf_pm (↑x) hn

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