Mathlib Map

Theorems · Theorem · functional analysis

IsPowMul.restriction

∀ {R : Type u_5} {S : Type u_6} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A : Subalgebra R S)
  {f : S → ℝ}, IsPowMul f → IsPowMul fun x => f ↑x

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

Defined in
Mathlib.Analysis.Normed.Ring.Basic
Cited by
1 results in Mathlib
Foundations
Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingRingAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

eq_of_powMul_faithful · cited by 1eq_of_powMul_faithfulReal · cited by 25697RealCommRing · cited by 17173CommRingAlgebra · cited by 11388AlgebraRing · cited by 7463RingSubalgebra · cited by 1353SubalgebraIsPowMul · cited by 39IsPowMulIsPowMul.restrictionCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement and proof · cited by 25,697
  • CommRingstatement and proof · cited by 17,173
  • Algebrastatement and proof · cited by 11,388
  • Ringstatement and proof · cited by 7,463
  • Subalgebrastatement and proof · cited by 1,353
  • IsPowMulstatement and proof · cited by 39

Cited by1

Results whose statement or proof uses this declaration.