Finiteness and surjectivity for WithOne #
WithOne α is finite when α is, and WithOne.lift f is surjective exactly when 1 and the
range of f cover the target.
theorem
WithOne.lift_surjective
{α : Type u_1}
{M : Type u_2}
[Mul α]
[MulOneClass M]
{f : α →ₙ* M}
:
Function.Surjective ⇑(lift f) ↔ ∀ (m : M), m = 1 ∨ m ∈ Set.range ⇑f