Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-08 20:17 5613d2ec

View on Github →

feat(tactic): add support for quotients to rcases

Estimated changes

Modified analysis/topology/topological_structures.lean

modified theorem continuous_multiset_sum

modified theorem tendsto_multiset_sum

Modified data/equiv/encodable.lean

Modified data/multiset.lean

modified theorem multiset.cons_inj_right

Modified data/quot.lean

modified theorem quotient.exact'

Modified docs/tactics.md

Modified group_theory/free_group.lean

modified def free_group.to_word.inj

modified def free_group.to_word.mk

Modified ring_theory/associated.lean

modified theorem associates.mul_zero

modified theorem associates.zero_mul

Modified ring_theory/unique_factorization_domain.lean

Modified set_theory/cardinal.lean

modified theorem cardinal.add_le_add

modified theorem cardinal.cantor

modified theorem cardinal.mul_le_mul

modified theorem cardinal.power_le_power_left

modified theorem cardinal.zero_le

Modified tactic/interactive.lean

Modified tactic/rcases.lean