Repository Issue Activity (beta)

#44009 Move away from unbundled relations in the `Ordinal` API

#42869 Rename `.lipschitz` to `.lipschitzWith`

#43952 Add a Group instance for LieEquiv (automorphisms of a Lie algebra / Lie module)

#17722 Define the Hodge star operator

#43872 Improve `Multipliable.inv` / `inv₀` docstrings for `ℂ` (and add `tprod_one_add_ne_zero_of_summable` cross-reference

#43870 Subscript and superscript parsers should produce round-tripping `Syntax`

#43855 Notation for multilinear maps

#39397 SetRel: Examples don't show why `α → β → Prop` is worse than `SetRel α β`

#43614 Bare `⊢ ℝ` unsolved goal when constructing IsPicardLindelof via of_time_independent with NNReal params

#15509 Proposal to add new attributes

#31365 Fixing Mathlib's morphism hierarchy

#34961 Graph theory def: Edge connectivity number

#43389 [misfiled — please ignore, closing]

#39639 Use `Is*Apply` classes

#28703 regression: if `norm_num at h1` closes a goal then `norm_num at h1 h2` fails

#38421 Strict group homs are stable by `Prod.map`

#28715 Show that `LieAlgebra.IsKilling.rootSystem` is right inverse to `RootPairing.GeckConstruction.lieAlgebra`

#6091 My 100 theorems

#33238 Add delaborator checking canonicity of instances

#42565 norm_num introduces Classical.choice on order goals over Nat/Int where decide does not

#6646 Make use of loopy instances for implications between Co(ntra)variantClasses

#43097 Fintype (Fin n) is resolved via SimplexCategory, producing non-normal terms

#38460 Define Fredholm operators

#41471 linarith? fails while linarith finds the proofs

#15865 lift tactic does not respect abbreviations