def «term#_» : Lean.ParserDescr

Equations

• «term#_» = Lean.ParserDescr.node `«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

theorem Sum.swap_inj {α β : Type} : Function.Injective Sum.swap

theorem finset_of_cardinality_between {α β : Type} [Fintype α] [Fintype β] {n : ℕ} (hα : #α < n) (hn : n ≤ #α + #β) : ∃ (b : Finset β), #(α ⊕ { x : β // x ∈ b }) = n ∧ Nonempty { x : β // x ∈ b }

theorem sum_over_fin_succ_of_only_zeroth_nonzero {α : Type} {n : ℕ} [AddCommMonoid α] {f : Fin n.succ → α} (hf : ∀ (i : Fin n.succ), i ≠ 0 → f i = 0) : Finset.univ.sum f = f 0

theorem zero_in_set_range_singType_cast {α : Type} [Ring α] : 0 ∈ Set.range SignType.cast

theorem in_set_range_singType_cast_mul_in_set_range_singType_cast {α : Type} [Ring α] {a b : α} (ha : a ∈ Set.range SignType.cast) (hb : b ∈ Set.range SignType.cast) : a * b ∈ Set.range SignType.cast

theorem neg_one_mul_in_set_range_singType_cast {α : Type} [Ring α] {a : α} (ha : a ∈ Set.range SignType.cast) : -1 * a ∈ Set.range SignType.cast

theorem in_set_range_singType_cast_of_neg_one_mul_self {α : Type} [Ring α] {a : α} (ha : -1 * a ∈ Set.range SignType.cast) : a ∈ Set.range SignType.cast

theorem in_set_range_singType_cast_iff_abs {α : Type} [LinearOrderedCommRing α] (a : α) : a ∈ Set.range SignType.cast ↔ |a| ∈ Set.range SignType.cast

theorem inv_eq_self_of_in_set_range_singType_cast {α : Type} [Field α] {a : α} (ha : a ∈ Set.range SignType.cast) : 1 / a = a