div_mul_div_comm for nat

Stream: Is there code for X?

[Chris Birkbeck]

Do we have

lemma nat_div_mul_div_comm (a b c d : ℕ) (ha : a ∣ b) (hc : c ∣ d) : (b*d)/(a*c) = (b/a)*(d/c) :=
begin
sorry,
end

?
We have div_mul_div_comm₀ but this is for comm_group_with_zero.

[Damiano Testa]

does docs#nat.div_mul_div_comm not work, as in (nat.div_mul_div_comm ha hc).symm?

[Chris Birkbeck]

Ha! it seems I almost guessed the name, but not quite!

[Chris Birkbeck]

That does work. Its funny that library_search couldnt find it.

[Damiano Testa]

Namespacing can be confusing, especially when it produces something that does not work with dot-notation...

[Damiano Testa]

Btw, I found it by writing div_mul_div_comm₀ in the online search tool. It produced no result, so I removed the trailing ₀ and it immediately showed div_mul_div_comm, nat.div_mul_div_comm as hits.

[Damiano Testa]

I suspect that div_mul_div_comm₀ was erased by one of Yaël's refactors.

[Yaël Dillies]

Yep, Damiano is exactly right. #14000

[Yaël Dillies]

For completeness, we should have nat.mul_div_mul_comm.