Mathlib Changelog v4

Changelog About Github

Theorem PiLp.add_apply

Modification history

2023-05-26 22:04

Mathlib/Analysis/NormedSpace/PiLp.lean

feat: port Analysis.NormedSpace.PiLp (#4345)

Added PiLp.add_apply View on Github →