Theorem preimage_smul_setₛₗ_of_isUnit_isUnit

Modification history