Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersFinset.card_filter_prod_self_eq
Plain-language statement
The diagonal of s × s has the same cardinality as s.
Source project: ArkLib
Person-level attribution pending.
Finset.card_prod_self_eq
Plain-language statement
The diagonal of s × s (intersection form) has the same cardinality as s.
Source project: ArkLib
Person-level attribution pending.
Ideal.principal_is_maximal_iff_irred
Project documentation
A principal ideal is an ideal generated by a single element. -/ def principalIdeal {F : Type} [Semiring F] (f : F) : Ideal F := Ideal.span {f} /- A principal ideal in a polynomial ring is maximal if and only if its generator is an irreducble polynomial.
Source project: ArkLib
Person-level attribution pending.
LinearCombination.linearCombination_ne_zero
Plain-language statement
A nonzero linear combination of linearly independent vectors is nonzero.
Source project: ArkLib
Person-level attribution pending.
Matrix.full_row_rank_via_rank_subLeftFull
Plain-language statement
An m×n matrix has full rank if the submatrix consisting of columns 1 through m has rank m.
Source project: ArkLib
Person-level attribution pending.
Univariate.separable_iff_discr_eq_zero
Plain-language statement
A polynomial is separable if and only if its discriminant is non-zero.
Source project: ArkLib
Person-level attribution pending.