## Stream: condensed mathematics

### Topic: Can r be 0?

#### 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?

#### Johan Commelin (Mar 26 2021 at 17:21):

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

#### 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