Theorem rpow_neg_one_add_norm_sq_le

Modification history

2023-06-13 06:31

Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

feat: port Analysis.SpecialFunctions.JapaneseBracket (#4924)

Added rpow_neg_one_add_norm_sq_le View on Github →