Commit 2024-06-17 15:40 12613ba8

View on Github →

chore(Analysis/Normed/Group): Move constructions (#13894) Split a new file Analysis.Normed.Group.Constructions off Analysis.Normed.Group.Basic.

Estimated changes

deleted theorem MulOpposite.nnnorm_op
deleted theorem MulOpposite.nnnorm_unop
deleted theorem MulOpposite.norm_op
deleted theorem MulOpposite.norm_unop
deleted theorem PUnit.norm_eq_zero
deleted theorem Pi.nnnorm_def'
deleted theorem Pi.norm_def'
deleted theorem Prod.nnorm_def
deleted theorem Prod.norm_def
deleted theorem ULift.nnnorm_def
deleted theorem ULift.nnnorm_down
deleted theorem ULift.nnnorm_up
deleted theorem ULift.norm_def
deleted theorem ULift.norm_down
deleted theorem ULift.norm_up
deleted theorem nnnorm_le_pi_nnnorm'
deleted theorem nnnorm_ofAdd
deleted theorem nnnorm_ofDual
deleted theorem nnnorm_ofMul
deleted theorem nnnorm_toAdd
deleted theorem nnnorm_toDual
deleted theorem nnnorm_toMul
deleted theorem norm_fst_le
deleted theorem norm_le_pi_norm'
deleted theorem norm_ofAdd
deleted theorem norm_ofDual
deleted theorem norm_ofMul
deleted theorem norm_prod_le_iff
deleted theorem norm_snd_le
deleted theorem norm_toAdd
deleted theorem norm_toDual
deleted theorem norm_toMul
deleted theorem pi_nnnorm_const'
deleted theorem pi_nnnorm_const_le'
deleted theorem pi_nnnorm_le_iff'
deleted theorem pi_nnnorm_lt_iff'
deleted theorem pi_norm_const'
deleted theorem pi_norm_const_le'
deleted theorem pi_norm_le_iff_of_nonneg'
deleted theorem pi_norm_lt_iff'
added theorem MulOpposite.nnnorm_op
added theorem MulOpposite.norm_op
added theorem MulOpposite.norm_unop
added theorem PUnit.norm_eq_zero
added theorem Pi.nnnorm_def'
added theorem Pi.norm_def'
added theorem Prod.nnorm_def
added theorem Prod.norm_def
added theorem ULift.nnnorm_def
added theorem ULift.nnnorm_down
added theorem ULift.nnnorm_up
added theorem ULift.norm_def
added theorem ULift.norm_down
added theorem ULift.norm_up
added theorem nnnorm_le_pi_nnnorm'
added theorem nnnorm_ofAdd
added theorem nnnorm_ofDual
added theorem nnnorm_ofMul
added theorem nnnorm_toAdd
added theorem nnnorm_toDual
added theorem nnnorm_toMul
added theorem norm_fst_le
added theorem norm_le_pi_norm'
added theorem norm_ofAdd
added theorem norm_ofDual
added theorem norm_ofMul
added theorem norm_prod_le_iff
added theorem norm_snd_le
added theorem norm_toAdd
added theorem norm_toDual
added theorem norm_toMul
added theorem pi_nnnorm_const'
added theorem pi_nnnorm_const_le'
added theorem pi_nnnorm_le_iff'
added theorem pi_nnnorm_lt_iff'
added theorem pi_norm_const'
added theorem pi_norm_const_le'
added theorem pi_norm_lt_iff'