Commit 2024-03-12 08:37 ada69fd3

View on Github →

chore(Nobeling): drop unneeded [Inhabited I] assumptions (#11310)

Estimated changes

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

modified theorem Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts

modified theorem Profinite.NobelingProof.Products.head!_le_of_lt

modified theorem Profinite.NobelingProof.Products.head_lt_ord_of_isGood

modified theorem Profinite.NobelingProof.Products.max_eq_eval

modified theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail'

modified theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail

modified theorem Profinite.NobelingProof.Products.rel_head!_of_mem