Timeroot

/- Define a "nonzero" type -/
import algebra.group
universe u
variables {M : Type*}
structure nonzero (α : Type u) [C : has_zero α] :=
(val : α)
(not_zero : val ≠ 0)
namespace nonzero
variable [has_zero M]
instance : has_coe (nonzero M) M := ⟨val⟩

Timeroot

import algebra.group_with_zero
import data.equiv.mul_add

universe u

variables {S : Type*}

--We're going to show the 1-to-1 correspondence between groups (with additive notation)
--and groups_with_zero (with multiplicative notation). To make the mapping less trivial,
--we'll also use the opposite group: so a+b becomes b*a.

Timeroot

int __cdecl main(int argc, const char **argv, const char **envp)
{
  const char *v3; // rcx@1
  __int16 v4; // ax@1
  unsigned __int8 v5; // ST17_1@1
  int v6; // eax@1
  int v7; // eax@1
  unsigned __int8 v8; // dl@1
  int v9; // eax@1
  int v10; // eax@1