Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-08 13:45 5acaeaf4

View on Github →

chore(computability/language): Golf (#13039) Golf the semiring instance using the set.image2 API, add half missing docstring.

Estimated changes

modified theorem language.mem_one
modified theorem language.mul_def
added theorem language.nil_mem_one
added theorem language.not_mem_zero