fixed measures

[faenuccio]

No description provided.

[jcommelin]

This currently has conflicts. Could you please look into those?

[faenuccio]

I think it is OK now. I have two comments though:

1. Theorems 2.4.14 and 2.2.6 seem two exact copies of one another. Should this be fixed?
2. In Section 2.2 I was using $\mathbb{Z}(\kern-.2em(T)\kern-.2em)$ (and likewise for square brackets) whereas in 2.4 it is $\mathbb{Z}((T))$ (different spacing between the brackets). Should this be uniformised?

[jcommelin]

@faenuccio Yes please, and yes please (-;

[faenuccio]

OK, I have performed all modifications; I have also observed that sometimes we wrote $\mathbb{Z}$ and sometimes $\mathbf{Z}$ (and similarly for the reals and naturals). I have uniformised everything.

[jcommelin]

Did you check whether this gives a connected dep-graph with all nodes coloured green? (If not, I can check it.)

[faenuccio]

Did you check whether this gives a connected dep-graph with all nodes coloured green? (If not, I can check it.)

No, I thought it could not be done on non-master branches. Can you check (and can you tell me how to get a graph on non-master branches?)

[jcommelin]

I get the following errors:

Lean declaration normed_group_hom.surjective_on_with not found
Lean declaration ses.continuous_θ_c not found
Lean declaration condensed.exact_of_exact_with_constant not found
Lean declaration thm69.θ_ϕ_exact not found

[faenuccio]

OK, let me have a look.