Can r be 0?

Stream: condensed mathematics

[Mario Carneiro]

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?

[Johan Commelin]

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

[Johan Commelin]

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