Commit 2024-01-26 03:03 e3b68186

View on Github →

fix: Clm -> CLM, Cle -> CLE (#10018) Rename

  • Complex.equivRealProdClmComplex.equivRealProdCLM;
    • TODO: should this one use CLE?
  • Complex.reClmComplex.reCLM;
  • Complex.imClmComplex.imCLM;
  • Complex.conjLieComplex.conjLIE;
  • Complex.conjCleComplex.conjCLE;
  • Complex.ofRealLiComplex.ofRealLI;
  • Complex.ofRealClmComplex.ofRealCLM;
  • fderivInnerClmfderivInnerCLM;
  • LinearPMap.adjointDomainMkClmLinearPMap.adjointDomainMkCLM;
  • LinearPMap.adjointDomainMkClmExtendLinearPMap.adjointDomainMkCLMExtend;
  • IsROrC.reClmIsROrC.reCLM;
  • IsROrC.imClmIsROrC.imCLM;
  • IsROrC.conjLieIsROrC.conjLIE;
  • IsROrC.conjCleIsROrC.conjCLE;
  • IsROrC.ofRealLiIsROrC.ofRealLI;
  • IsROrC.ofRealClmIsROrC.ofRealCLM;
  • MeasureTheory.condexpL1ClmMeasureTheory.condexpL1CLM;
  • algebraMapClmalgebraMapCLM;
  • WeakDual.CharacterSpace.toClmWeakDual.CharacterSpace.toCLM;
  • BoundedContinuousFunction.evalClmBoundedContinuousFunction.evalCLM;
  • ContinuousMap.evalClmContinuousMap.evalCLM;
  • TrivSqZeroExt.fstClmTrivSqZeroExt.fstClm;
  • TrivSqZeroExt.sndClmTrivSqZeroExt.sndCLM;
  • TrivSqZeroExt.inlClmTrivSqZeroExt.inlCLM;
  • TrivSqZeroExt.inrClmTrivSqZeroExt.inrCLM and related theorems.

Estimated changes

added def Complex.conjCLE
added theorem Complex.conjCLE_apply
added theorem Complex.conjCLE_coe
deleted def Complex.conjCle
deleted theorem Complex.conjCle_apply
deleted theorem Complex.conjCle_coe
added def Complex.conjLIE
added theorem Complex.conjLIE_apply
added theorem Complex.conjLIE_symm
deleted def Complex.conjLie
deleted theorem Complex.conjLie_apply
deleted theorem Complex.conjLie_symm
added def Complex.imCLM
added theorem Complex.imCLM_apply
added theorem Complex.imCLM_coe
deleted def Complex.imClm
deleted theorem Complex.imClm_apply
deleted theorem Complex.imClm_coe
added theorem Complex.ofRealCLM_coe
deleted def Complex.ofRealClm
deleted theorem Complex.ofRealClm_apply
deleted theorem Complex.ofRealClm_coe
added def Complex.ofRealLI
deleted def Complex.ofRealLi
added def Complex.reCLM
added theorem Complex.reCLM_apply
added theorem Complex.reCLM_coe
deleted def Complex.reClm
deleted theorem Complex.reClm_apply
deleted theorem Complex.reClm_coe
added theorem Complex.conjCLE_nnorm
added theorem Complex.conjCLE_norm
deleted theorem Complex.conjCle_nnorm
deleted theorem Complex.conjCle_norm
added theorem Complex.det_conjLIE
deleted theorem Complex.det_conjLie
added theorem Complex.imCLM_nnnorm
added theorem Complex.imCLM_norm
deleted theorem Complex.imClm_nnnorm
deleted theorem Complex.imClm_norm
added theorem Complex.ofRealCLM_norm
deleted theorem Complex.ofRealClm_nnnorm
deleted theorem Complex.ofRealClm_norm
added theorem Complex.reCLM_nnnorm
added theorem Complex.reCLM_norm
deleted theorem Complex.reClm_nnnorm
deleted theorem Complex.reClm_norm
added theorem IsROrC.conjCLE_apply
added theorem IsROrC.conjCLE_coe
deleted theorem IsROrC.conjCle_apply
deleted theorem IsROrC.conjCle_coe
added theorem IsROrC.conjLIE_apply
deleted theorem IsROrC.conjLie_apply
added theorem IsROrC.imCLM_apply
added theorem IsROrC.imCLM_coe
deleted theorem IsROrC.imClm_apply
deleted theorem IsROrC.imClm_coe
added theorem IsROrC.ofRealCLM_apply
added theorem IsROrC.ofRealCLM_coe
deleted theorem IsROrC.ofRealClm_apply
deleted theorem IsROrC.ofRealClm_coe
added theorem IsROrC.ofRealLI_apply
deleted theorem IsROrC.ofRealLi_apply
added theorem IsROrC.reCLM_apply
added theorem IsROrC.reCLM_coe
deleted theorem IsROrC.reClm_apply
deleted theorem IsROrC.reClm_coe