Commit 2024-01-26 03:03 e3b68186

View on Github →

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

  • Complex.equivRealProdClm → Complex.equivRealProdCLM;
    • TODO: should this one use CLE?
  • Complex.reClm → Complex.reCLM;
  • Complex.imClm → Complex.imCLM;
  • Complex.conjLie → Complex.conjLIE;
  • Complex.conjCle → Complex.conjCLE;
  • Complex.ofRealLi → Complex.ofRealLI;
  • Complex.ofRealClm → Complex.ofRealCLM;
  • fderivInnerClm → fderivInnerCLM;
  • LinearPMap.adjointDomainMkClm → LinearPMap.adjointDomainMkCLM;
  • LinearPMap.adjointDomainMkClmExtend → LinearPMap.adjointDomainMkCLMExtend;
  • IsROrC.reClm → IsROrC.reCLM;
  • IsROrC.imClm → IsROrC.imCLM;
  • IsROrC.conjLie → IsROrC.conjLIE;
  • IsROrC.conjCle → IsROrC.conjCLE;
  • IsROrC.ofRealLi → IsROrC.ofRealLI;
  • IsROrC.ofRealClm → IsROrC.ofRealCLM;
  • MeasureTheory.condexpL1Clm → MeasureTheory.condexpL1CLM;
  • algebraMapClm → algebraMapCLM;
  • WeakDual.CharacterSpace.toClm → WeakDual.CharacterSpace.toCLM;
  • BoundedContinuousFunction.evalClm → BoundedContinuousFunction.evalCLM;
  • ContinuousMap.evalClm → ContinuousMap.evalCLM;
  • TrivSqZeroExt.fstClm → TrivSqZeroExt.fstClm;
  • TrivSqZeroExt.sndClm → TrivSqZeroExt.sndCLM;
  • TrivSqZeroExt.inlClm → TrivSqZeroExt.inlCLM;
  • TrivSqZeroExt.inrClm → TrivSqZeroExt.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