Skip to content

Commit

Permalink
chore: add shortcut T2Space ℂ instance (#11222)
Browse files Browse the repository at this point in the history
This adds a shortcut instance for `T2Space ℂ` in `Analysis.Complex.Basic`.

See [this thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.22.23synth.20T2Space.20.E2.84.82.22.20fails/near/425351881) on Zulip.
  • Loading branch information
MichaelStollBayreuth committed Mar 7, 2024
1 parent c5eaf25 commit b10f73d
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions Mathlib/Analysis/Complex/Basic.lean
Expand Up @@ -238,6 +238,8 @@ theorem uniformEmbedding_equivRealProd : UniformEmbedding equivRealProd :=
instance : CompleteSpace ℂ :=
(completeSpace_congr uniformEmbedding_equivRealProd).mpr inferInstance

instance instT2Space : T2Space ℂ := TopologicalSpace.t2Space_of_metrizableSpace

/-- The natural `ContinuousLinearEquiv` from `ℂ` to `ℝ × ℝ`. -/
@[simps! (config := { simpRhs := true }) apply symm_apply_re symm_apply_im]
def equivRealProdCLM : ℂ ≃L[ℝ] ℝ × ℝ :=
Expand Down

0 comments on commit b10f73d

Please sign in to comment.