mathlib3
c2debc48 - refactor(combinatorics/configuration): Implicit arguments for `nondegenerate.eq_or_eq` (#10885)

Commit
4 years ago
refactor(combinatorics/configuration): Implicit arguments for `nondegenerate.eq_or_eq` (#10885) The arguments `p₁`, `p₂`, `l₁`, `l₂` can be implicit, since they can be inferred from `p₁ ∈ l₁`, `p₂ ∈ l₁`, `p₁ ∈ l₂`, `p₂ ∈ l₂`.
Author
Parents
Loading