Zulip Chat Archive

Stream: condensed mathematics

Topic: Can r be 0?


view this post on Zulip Mario Carneiro (Mar 26 2021 at 17:15):

I'm playing with the rescale_iso refactor and we have

def Tinv₀ (c c₂ : 0) [h : fact (c  r' * c₂)] (x : filtration M c) : filtration M c₂ :=
Tinv (x : M), filtration_mono (aux h.1) (Tinv_mem_filtration _ _ x.2)⟩

in with_Tinv that is supposed to be a generalization of the original Tinv₀ that fixes c₂ = r'⁻¹ * c. But this requires c ≤ r' * (r'⁻¹ * c), and I don't see an assumption that r' is not zero?

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:21):

@Mario Carneiro You can add that assumption wherever you need it

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:22):

It's just that the linter occasionally points out that we aren't using that r' is nonzero. But in then end both r and r' will be nonzero


Last updated: May 09 2021 at 22:13 UTC