Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-03 02:24 0a4fbd8c

View on Github →

chore(data/prod): add prod.forall' and prod.exists' (#5570) They work a bit better with curried functions.

Estimated changes

added theorem prod.exists'
deleted theorem prod.exists
added theorem prod.forall'
deleted theorem prod.forall
added theorem prod.«exists»
added theorem prod.«forall»