Commit 2024-08-06 04:16 994b33b7

View on Github →

chore(*): rename Cstar* to CStar* (#15495) Moves:

Cstar* -> CStar*

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Analysis/CstarAlgebra/Basic.lean to Mathlib/Analysis/CStarAlgebra/Basic.lean

added theorem CStarRing.mul_star_self_eq_zero_iff

added theorem CStarRing.mul_star_self_ne_zero_iff

added theorem CStarRing.nnnorm_self_mul_star

added theorem CStarRing.nnnorm_star_mul_self

added theorem CStarRing.norm_coe_unitary

added theorem CStarRing.norm_coe_unitary_mul

added theorem CStarRing.norm_mem_unitary_mul

added theorem CStarRing.norm_mul_coe_unitary

added theorem CStarRing.norm_mul_mem_unitary

added theorem CStarRing.norm_of_mem_unitary

added theorem CStarRing.norm_one

added theorem CStarRing.norm_self_mul_star

added theorem CStarRing.norm_star_mul_self'

added theorem CStarRing.norm_star_mul_self

added theorem CStarRing.norm_unitary_smul

added theorem CStarRing.star_mul_self_eq_zero_iff

added theorem CStarRing.star_mul_self_ne_zero_iff

deleted theorem CstarRing.mul_star_self_eq_zero_iff

deleted theorem CstarRing.mul_star_self_ne_zero_iff

deleted theorem CstarRing.nnnorm_self_mul_star

deleted theorem CstarRing.nnnorm_star_mul_self

deleted theorem CstarRing.norm_coe_unitary

deleted theorem CstarRing.norm_coe_unitary_mul

deleted theorem CstarRing.norm_mem_unitary_mul

deleted theorem CstarRing.norm_mul_coe_unitary

deleted theorem CstarRing.norm_mul_mem_unitary

deleted theorem CstarRing.norm_of_mem_unitary

deleted theorem CstarRing.norm_one

deleted theorem CstarRing.norm_self_mul_star

deleted theorem CstarRing.norm_star_mul_self'

deleted theorem CstarRing.norm_star_mul_self

deleted theorem CstarRing.norm_unitary_smul

deleted theorem CstarRing.star_mul_self_eq_zero_iff

deleted theorem CstarRing.star_mul_self_ne_zero_iff

modified theorem IsSelfAdjoint.nnnorm_pow_two_pow

modified theorem selfAdjoint.nnnorm_pow_two_pow

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Basic.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Instances.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

added def CStarRing.spectralOrder

added theorem CStarRing.spectralOrderedRing

deleted def CstarRing.spectralOrder

deleted theorem CstarRing.spectralOrderedRing

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Order.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

added theorem CStarRing.conjugate_le_norm_smul'

added theorem CStarRing.conjugate_le_norm_smul

added theorem CStarRing.mul_star_le_algebraMap_norm_sq

added theorem CStarRing.nnnorm_mem_spectrum_of_nonneg

added theorem CStarRing.norm_le_norm_of_nonneg_of_le

added theorem CStarRing.norm_mem_spectrum_of_nonneg

added theorem CStarRing.norm_or_neg_norm_mem_spectrum

added theorem CStarRing.star_mul_le_algebraMap_norm_sq

deleted theorem CstarRing.conjugate_le_norm_smul'

deleted theorem CstarRing.conjugate_le_norm_smul

deleted theorem CstarRing.mul_star_le_algebraMap_norm_sq

deleted theorem CstarRing.nnnorm_mem_spectrum_of_nonneg

deleted theorem CstarRing.norm_le_norm_of_nonneg_of_le

deleted theorem CstarRing.norm_mem_spectrum_of_nonneg

deleted theorem CstarRing.norm_or_neg_norm_mem_spectrum

deleted theorem CstarRing.star_mul_le_algebraMap_norm_sq

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Restrict.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Unique.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Unital.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Renamed Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Unitary.lean to Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean

Renamed Mathlib/Analysis/CstarAlgebra/Exponential.lean to Mathlib/Analysis/CStarAlgebra/Exponential.lean

Renamed Mathlib/Analysis/CstarAlgebra/GelfandDuality.lean to Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

Renamed Mathlib/Analysis/CstarAlgebra/Matrix.lean to Mathlib/Analysis/CStarAlgebra/Matrix.lean

added theorem Matrix.instCStarRing

deleted theorem Matrix.instCstarRing

Renamed Mathlib/Analysis/CstarAlgebra/Module.lean to Mathlib/Analysis/CStarAlgebra/Module.lean

added theorem CStarModule.continuous_inner

added theorem CStarModule.innerSL_apply

added theorem CStarModule.inner_add_left

added theorem CStarModule.inner_mul_inner_swap_le

added theorem CStarModule.inner_neg_left

added theorem CStarModule.inner_neg_right

added theorem CStarModule.inner_op_smul_left

added theorem CStarModule.inner_self_eq_norm_sq

added theorem CStarModule.inner_smul_left_complex

added theorem CStarModule.inner_smul_left_real

added theorem CStarModule.inner_smul_right_real

added theorem CStarModule.inner_sub_left

added theorem CStarModule.inner_sub_right

added theorem CStarModule.inner_sum_left

added theorem CStarModule.inner_sum_right

added theorem CStarModule.inner_zero_left

added theorem CStarModule.inner_zero_right

added def CStarModule.innerₛₗ

added theorem CStarModule.innerₛₗ_apply

added theorem CStarModule.isSelfAdjoint_inner_self

added theorem CStarModule.norm_eq_csSup

added theorem CStarModule.norm_inner_le

added theorem CStarModule.norm_sq_eq

added theorem CStarModule.norm_zero_iff

added theorem CStarModule.normedSpaceCore

deleted theorem CstarModule.continuous_inner

deleted theorem CstarModule.innerSL_apply

deleted theorem CstarModule.inner_add_left

deleted theorem CstarModule.inner_mul_inner_swap_le

deleted theorem CstarModule.inner_neg_left

deleted theorem CstarModule.inner_neg_right

deleted theorem CstarModule.inner_op_smul_left

deleted theorem CstarModule.inner_self_eq_norm_sq

deleted theorem CstarModule.inner_smul_left_complex

deleted theorem CstarModule.inner_smul_left_real

deleted theorem CstarModule.inner_smul_right_real

deleted theorem CstarModule.inner_sub_left

deleted theorem CstarModule.inner_sub_right

deleted theorem CstarModule.inner_sum_left

deleted theorem CstarModule.inner_sum_right

deleted theorem CstarModule.inner_zero_left

deleted theorem CstarModule.inner_zero_right

deleted def CstarModule.innerₛₗ

deleted theorem CstarModule.innerₛₗ_apply

deleted theorem CstarModule.isSelfAdjoint_inner_self

deleted theorem CstarModule.norm_eq_csSup

deleted theorem CstarModule.norm_inner_le

deleted theorem CstarModule.norm_sq_eq

deleted theorem CstarModule.norm_zero_iff

deleted theorem CstarModule.normedSpaceCore

Renamed Mathlib/Analysis/CstarAlgebra/Multiplier.lean to Mathlib/Analysis/CStarAlgebra/Multiplier.lean

Renamed Mathlib/Analysis/CstarAlgebra/Spectrum.lean to Mathlib/Analysis/CStarAlgebra/Spectrum.lean

Renamed Mathlib/Analysis/CstarAlgebra/Unitization.lean to Mathlib/Analysis/CStarAlgebra/Unitization.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/Matrix.lean

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean

Modified Mathlib/Analysis/Quaternion.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

Modified Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified Mathlib/Topology/ContinuousFunction/Compact.lean

Modified Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

Modified scripts/noshake.json

Modified test/TCSynth.lean