## Stream: maths

### Topic: complex.ext_iff a simp lemma?

#### Reid Barton (May 28 2020 at 14:29):

On a somewhat related note, I wonder whether ext should only locally be an ext lemma.

#### Reid Barton (May 28 2020 at 14:31):

If you have two, I don't know, bundled holomorphic functions and you want to prove they're equal because they're pointwise equal, probably you do not want to split into real and imaginary components.

Last updated: May 18 2021 at 06:15 UTC