[Merged by Bors] - feat(data/nat/mul_ind): multiplicative induction principles

[ericrbg]

Co-authored-by: Eric Wieser wieser.eric@gmail.com

---

whilst writing up the docstring, I realised that the question of uniqueness never really came to mind, which is probably important as these are Sort* valued, instead of just Prop.

[Vierkantor]

Interestingly, I just proved induction_on_coprime for unique factorization domains. But you can't in good faith return data from that one, since factorization in UFDs is only unique up to units, so I think these recursion principles on ℕ are useful.

Although you might want to generalize to UFD + normalization_domain if you have some time left over... :P

[Vierkantor]

Would the div section of data.nat.basic work for this one, or is that too early?

[ericrbg]

woo! I found both sides of the implication there so less code ^^

[ericrbg]

Thanks Anne! As soon as I get a spare bit I'll try see if I can generalize this, I didn't know about normalization_monoid, so hopefully the API there is good enough :) How does the "get any prime" look over there - here I use min_fac, but will I have to do some classical.some faffing?

[Vierkantor]

Thanks Anne! As soon as I get a spare bit I'll try see if I can generalize this, I didn't know about normalization_monoid, so hopefully the API there is good enough :)

Well, you can try, but if it turns out to be a huge pile of work, please don't spend too much time!

How does the "get any prime" look over there - here I use min_fac, but will I have to do some classical.some faffing?

My approach was to first show the result for a finset.prod of powers of pairwise coprime prime elements, and then translate the multiset of factors to a finset that satisfies the assumptions. The difficult part is choosing everything uniquely, because here I do it up to associated.

[ericrbg]

I tried a little with normalization_monoid, and quickly grew overwhelmed, so in fact I'll leave it as a note to future work. I'm planning to work on this stuff a bit more (refactoring padic_val_prime to hopefully require far less imports, too), but for now I think it'd be nice to have these in, and hopefully work on them later! (I'll put the note in a bit, I have a sneaky feeling this build is going to fail...)

[Vierkantor]

I still can't think of a good alternative name for rec_on_coprime', so I made a Zulip thread.

LGTM otherwise.

[Vierkantor]

I agree with @eric-wieser's suggestions in the Zulip thread. LGTM otherwise, so:

bors d+

[bors]

✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ericrbg]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests