Theorem nndist_mulIndicator

Modification history

2023-08-23 11:25

Mathlib/Analysis/Normed/Group/Basic.lean

feat: lemmas about indicator of the symmetric difference (#6738)

Added nndist_mulIndicator View on Github →