Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 18:26 e43d9649

View on Github →

chore(data/pi,algebra/group/pi): reorganize proofs (#6869) Add pi.single_op and pi.single_binop and use them in the proofs.

Estimated changes

modified def mul_hom.single
modified theorem pi.single_mul
deleted theorem pi.single_zero
added theorem pi.mul_def
modified theorem pi.single_eq_of_ne
modified theorem pi.single_eq_same
added theorem pi.single_op
added theorem pi.single_op₂
added theorem pi.single_zero