no_zero_smul_divisors

Stream: general

[Eric Rodriguez]

we have a fair few theorems stating that some algebra map is injective. we also have docs#no_zero_smul_divisors, which is essentially that fact but made available to TC; can we start adding instances such as no_zero_smul_divisors A K for is_fraction_ring A K? (docs#is_fraction_ring.injective)? If so, should we also _remove_ these explicit algebra_map_injectives and use docs#no_zero_smul_divisors.algebra_map_injective? In that case, should we even rename this to algebra_map_injective, and then basically have it documented that if you want injective(algebra_map), you should basically try this magic incantation? Or is that too noob-unfriendly

[Eric Rodriguez]

I'm very happy with any solution, but I'd quite like the instances... I'll put a poll up too

[Eric Rodriguez]

/poll What to do with injective algebra_maps?
Move everything to no_smul_zero_divisors + rename no_smul_zero_divisors.algebra_map_injective
Move everything to no_smul_zero_divisors without the rename
Leave both options available
Don't move anything to no_smul_zero_divisors

[Andrew Yang]

Why didn't we make function.injective a class in the first place?

[Eric Rodriguez]

My fuzzy memory tells me it used to be, then issues came up; maybe this is sort of what Anne's fun_like things are building up to (the "correct" approach to turning things like this into classes)

[Reid Barton]

I mean, in general you don't want things to be classes by default because classes are a pain

[Andrew Yang]

Why so? I've not yet been bitten by a Prop valued class.

[Reid Barton]

They make it harder to just prove stuff

[Andrew Yang]

Its probably because of my lack of experience that I have not yet ran into any problems, but I think the category theory part of mathlib uses classes quite extensively and yet it is quite easy to use?

[Eric Rodriguez]

I just wanna bump this before I start a refactor and then find out people have opinions on how this should be done

[Eric Rodriguez]

(although maybe this is inadvisable considering how many problems I'm having with this specific class in FLT-regular, c.f. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/TC.20hell.20in.20FLT-regular)