Theorem Matrix.frobeniusBoundedSMul

Modification history

2025-03-11 08:53

Mathlib/Analysis/Matrix.lean

chore(Topology/MetricSpace): rename BoundedSMul to IsBoundedSMul (#22797) …

Deleted Matrix.frobeniusBoundedSMul View on Github →

2024-01-20 16:06

Mathlib/Analysis/Matrix.lean

feat: `BoundedSMul` for matrix norms (#9817) …

Added Matrix.frobeniusBoundedSMul View on Github →