Commit 2023-05-25 03:53 b399e6a7

View on Github →

feat: port Analysis.NormedSpace.Star.Multiplier (#4312)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

added theorem DoubleCentralizer.add_fst

added theorem DoubleCentralizer.add_snd

added theorem DoubleCentralizer.add_toProd

added theorem DoubleCentralizer.algebraMap_fst

added theorem DoubleCentralizer.algebraMap_snd

added theorem DoubleCentralizer.algebraMap_toProd

added theorem DoubleCentralizer.coe_eq_algebraMap

added theorem DoubleCentralizer.coe_fst

added theorem DoubleCentralizer.coe_snd

added theorem DoubleCentralizer.ext

added theorem DoubleCentralizer.int_cast_fst

added theorem DoubleCentralizer.int_cast_snd

added theorem DoubleCentralizer.int_cast_toProd

added theorem DoubleCentralizer.mul_fst

added theorem DoubleCentralizer.mul_snd

added theorem DoubleCentralizer.nat_cast_fst

added theorem DoubleCentralizer.nat_cast_snd

added theorem DoubleCentralizer.nat_cast_toProd

added theorem DoubleCentralizer.neg_fst

added theorem DoubleCentralizer.neg_snd

added theorem DoubleCentralizer.neg_toProd

added theorem DoubleCentralizer.nnnorm_def'

added theorem DoubleCentralizer.nnnorm_def

added theorem DoubleCentralizer.nnnorm_fst

added theorem DoubleCentralizer.nnnorm_fst_eq_snd

added theorem DoubleCentralizer.nnnorm_snd

added theorem DoubleCentralizer.norm_def'

added theorem DoubleCentralizer.norm_def

added theorem DoubleCentralizer.norm_fst

added theorem DoubleCentralizer.norm_fst_eq_snd

added theorem DoubleCentralizer.norm_snd

added theorem DoubleCentralizer.one_fst

added theorem DoubleCentralizer.one_snd

added theorem DoubleCentralizer.one_toProd

added theorem DoubleCentralizer.pow_fst

added theorem DoubleCentralizer.pow_snd

added theorem DoubleCentralizer.pow_toProd

added theorem DoubleCentralizer.range_toProd

added theorem DoubleCentralizer.range_toProdMulOpposite

added theorem DoubleCentralizer.smul_fst

added theorem DoubleCentralizer.smul_snd

added theorem DoubleCentralizer.smul_toProd

added theorem DoubleCentralizer.star_fst

added theorem DoubleCentralizer.star_snd

added theorem DoubleCentralizer.sub_fst

added theorem DoubleCentralizer.sub_snd

added theorem DoubleCentralizer.sub_toProd

added def DoubleCentralizer.toProdHom

added def DoubleCentralizer.toProdMulOpposite

added def DoubleCentralizer.toProdMulOppositeHom

added theorem DoubleCentralizer.toProdMulOpposite_injective

added theorem DoubleCentralizer.uniformEmbedding_toProdMulOpposite

added theorem DoubleCentralizer.zero_fst

added theorem DoubleCentralizer.zero_snd

added theorem DoubleCentralizer.zero_toProd

added structure DoubleCentralizer