Mathlib references

Every Mathlib declaration referred to directly by this project’s own code, grouped by the module it comes from.

definition abbreviation theorem

legend

`Algebra.BigOperators.Fin`

Fin.sum_univ_add

theorem Fin.sum_univ_add.{u_2} {M : Type u_2} [AddCommMonoid M] {a b : ℕ} (f : Fin (a + b) → M) :
  ∑ i, f i = ∑ i, f (Fin.castAdd b i) + ∑ i, f (Fin.natAdd a i)

Used by: Component.Impl.parallel, Component.Impl.symmetry

Fin.sum_univ_one

theorem Fin.sum_univ_one.{u_2} {M : Type u_2} [AddCommMonoid M] (f : Fin 1 → M) : ∑ i, f i = f 0

Used by: Component.Impl.Simplex.toInformationSystem, InformationSystem.toSimplex

Fin.sum_univ_two

theorem Fin.sum_univ_two.{u_2} {M : Type u_2} [AddCommMonoid M] (f : Fin 2 → M) : ∑ i, f i = f 0 + f 1

Used by: InformationSystem.parallel_delta

`Algebra.BigOperators.Group.Finset.Basic`

Finset.sum_congr

theorem Finset.sum_congr.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M]
  {f g : ι → M} (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g

Used by: Component.Func.toImpl, Component.Impl.empty, Component.Impl.id, Component.Impl.parallel, Component.Impl.symmetry, Discrete.pi

`Algebra.BigOperators.Group.Finset.Defs`

Finset.sum

∑ x ∈ s, f x is the sum of f x as x ranges over the elements of the finite set s.

When the index type is a Fintype, the notation ∑ x, f x, is a shorthand for ∑ x ∈ Finset.univ, f x.

def Finset.sum.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : M

Used by: Component.Func.toImpl, Component.Impl.Simplex.toInformationSystem, Component.Impl.id, Component.Impl.parallel, Component.Impl.symmetry, Discrete.pi, InformationSystem.parallel_delta, InformationSystem.toSimplex, instNormForallFin_computerNetworks, instNormValue

`Algebra.BigOperators.Ring.Finset`

Nat.cast_sum

theorem Nat.cast_sum.{u_4, u_5} {R : Type u_4} {ι : Type u_5} [AddCommMonoidWithOne R] (s : Finset ι)
  (f : ι → ℕ) : ↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)

Used by: Discrete.pi

`Algebra.Group.Basic`

neg_eq_zero

theorem neg_eq_zero.{u_1} {α : Type u_1} [SubtractionMonoid α] {a : α} : -a = 0 ↔ a = 0

Used by: Component.Impl.Simplex.toInformationSystem, Component.Impl.parallel, Component.Impl.sequential, InformationSystem.Environment.universe, InformationSystem.Step.bottom, InformationSystem.Step.delta_alt, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.eval_delta, InformationSystem.roundtrip_neutral, InformationSystem.toSimplex, InformationSystem.zero_run_le, irrational_logb_two_three

sub_add_sub_cancel

theorem sub_add_sub_cancel.{u_3} {G : Type u_3} [AddGroup G] (a b c : G) : a - b + (b - c) = a - c

Used by: InformationSystem.sequential_delta

sub_eq_zero_of_eq

Alias of the reverse direction of sub_eq_zero.

theorem sub_eq_zero_of_eq.{u_3} {G : Type u_3} [AddGroup G] {a b : G} : a = b → a - b = 0

`Algebra.Group.Defs`

add_zero

theorem add_zero.{u} {M : Type u} [AddZeroClass M] (a : M) : a + 0 = a

Used by: Component.Impl.empty, eraseSecondBit

one_pow

theorem one_pow.{u_2} {M : Type u_2} [Monoid M] (n : ℕ) : 1 ^ n = 1

Used by: no_pow_two_eq_pow_three

pow_add

theorem pow_add.{u_2} {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n

Used by: card_BitFunction_succ_output

pow_mul

theorem pow_mul.{u_2} {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ (m * n) = (a ^ m) ^ n

Used by: card_BitFunction, card_BitFunction_succ_input

pow_succ

theorem pow_succ.{u_2} {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a

Used by: card_BitFunction_succ_input, no_pow_two_eq_pow_three

pow_zero

theorem pow_zero.{u_2} {M : Type u_2} [Monoid M] (a : M) : a ^ 0 = 1

Used by: no_pow_two_eq_pow_three

sub_self

theorem sub_self.{u_1} {G : Type u_1} [AddGroup G] (a : G) : a - a = 0

Used by: InformationSystem.eval_delta

zero_add

theorem zero_add.{u} {M : Type u} [AddZeroClass M] (a : M) : 0 + a = a

Used by: Component.Func.toImpl, Component.Impl.empty_parallel, Component.Impl.id

`Algebra.GroupWithZero.Units.Basic`

div_eq_iff

theorem div_eq_iff.{u_3} {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
  a / b = c ↔ a = c * b

Used by: irrational_logb_two_three

`Algebra.Order.BigOperators.Group.Finset`

Finset.sum_nonneg

theorem Finset.sum_nonneg.{u_1, u_5} {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [Preorder N]
  {f : ι → N} {s : Finset ι} [AddLeftMono N] (h : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∑ i ∈ s, f i

Used by: instNormNonnegForallFin

`Algebra.Order.Monoid.Unbundled.Basic`

add_nonneg

Alias of Left.add_nonneg.

theorem add_nonneg.{u_1} {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a b : α} (ha : 0 ≤ a)
  (hb : 0 ≤ b) : 0 ≤ a + b

Used by: instNormNonnegProd

`Algebra.Order.Ring.Unbundled.Rat`

Rat.num_pos

theorem Rat.num_pos {a : ℚ} : 0 < a.num ↔ 0 < a

Used by: irrational_logb_two_three

`Algebra.Order.Sub.Defs`

add_tsub_cancel_left

theorem add_tsub_cancel_left.{u_1} {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α]
  [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a + b - a = b

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse

`Algebra.Ring.Defs`

Ring

A Ring is a Semiring with negation making it an additive group.

structure Ring.{u} (R : Type u) : Type u

add_one_mul

theorem add_one_mul.{u} {α : Type u} [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
  (a + 1) * b = a * b + b

Used by: card_BitFunction_succ_output

`Algebra.Ring.Rat`

Rat.num_div_den

theorem Rat.num_div_den (r : ℚ) : ↑r.num / ↑r.den = r

Used by: irrational_logb_two_three

`Analysis.Normed.Group.Defs`

Norm

Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ‖x‖. This class is designed to be extended in more interesting classes specifying the properties of the norm.

structure Norm.{u_8} (E : Type u_8) : Type u_8

`Analysis.SpecialFunctions.Log.Base`

Real.logb

The real logarithm in a given base. As with the natural logarithm, we define logb b x to be logb b |x| for x < 0, and 0 for x = 0.

def Real.logb (b x : ℝ) : ℝ

Used by: irrational_logb_two_three, traffic_light_information

Real.rpow_logb

theorem Real.rpow_logb {b x : ℝ} (b_pos : 0 < b) (b_ne_one : b ≠ 1) (hx : 0 < x) : b ^ Real.logb b x = x

Used by: irrational_logb_two_three

`Analysis.SpecialFunctions.Pow.Real`

Real.rpow_lt_rpow_left_iff

theorem Real.rpow_lt_rpow_left_iff {x y z : ℝ} (hx : 1 < x) : x ^ y < x ^ z ↔ y < z

Used by: irrational_logb_two_three

Real.rpow_mul

theorem Real.rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z

Used by: irrational_logb_two_three

Real.rpow_natCast

theorem Real.rpow_natCast (x : ℝ) (n : ℕ) : x ^ ↑n = x ^ n

Used by: irrational_logb_two_three

Real.rpow_zero

theorem Real.rpow_zero (x : ℝ) : x ^ 0 = 1

Used by: irrational_logb_two_three

`CategoryTheory.Category.Basic`

CategoryTheory.Category

The typeclass Category C describes morphisms associated to objects of type C. The universe levels of the objects and morphisms are unconstrained, and will often need to be specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.)

structure CategoryTheory.Category.{v, u} (obj : Type u) : Type (max u (v + 1))

Used by: Component.Func.category, Component.Impl.category, Component.Spec.category, instCategoryPROP, instCategoryPROP_1, instCategoryPROP_2

`CategoryTheory.EqToHom`

CategoryTheory.eqToHom

An equality X = Y gives us a morphism X ⟶ Y.

It is typically better to use this, rather than rewriting by the equality then using 1 _ which usually leads to dependent type theory hell.

def CategoryTheory.eqToHom.{v₁, u₁} {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : X ⟶ Y

Used by: Component.Func.braidedCategory, Component.Func.comp_eqToHom, Component.Func.eqToHom_comp, Component.Func.eqToHom_eq_recast_id, Component.Func.monoidalCategory, Component.Func.recast_eqToHom, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.eqToHom_eq_recast_id, Component.Impl.Hom.recast_eqToHom, Component.Impl.braidedCategory, Component.Impl.monoidalCategory, Component.Spec.braidedCategory, Component.Spec.comp_eqToHom, Component.Spec.eqToHom_comp, Component.Spec.eqToHom_eq_recast_id, Component.Spec.monoidalCategory, Component.Spec.recast_eqToHom

CategoryTheory.eqToIso

An equality X = Y gives us an isomorphism X ≅ Y.

It is typically better to use this, rather than rewriting by the equality then using Iso.refl _ which usually leads to dependent type theory hell.

def CategoryTheory.eqToIso.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : X ≅ Y

Used by: Component.Func.braidedCategory, Component.Func.monoidalCategory, Component.Func.monoidalCategoryStruct, Component.Impl.braidedCategory, Component.Impl.monoidalCategory, Component.Impl.monoidalCategoryStruct, Component.Spec.braidedCategory, Component.Spec.monoidalCategory, Component.Spec.monoidalCategoryStruct

CategoryTheory.eqToIso.hom

theorem CategoryTheory.eqToIso.hom.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : (CategoryTheory.eqToIso p).hom = CategoryTheory.eqToHom p

Used by: Component.Func.braidedCategory, Component.Func.monoidalCategory, Component.Impl.braidedCategory, Component.Impl.monoidalCategory, Component.Spec.braidedCategory, Component.Spec.monoidalCategory

CategoryTheory.eqToIso.inv

theorem CategoryTheory.eqToIso.inv.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (p : X = Y) : (CategoryTheory.eqToIso p).inv = CategoryTheory.eqToHom ⋯

Used by: Component.Func.braidedCategory, Component.Impl.braidedCategory, Component.Spec.braidedCategory

`CategoryTheory.Functor.Basic`

CategoryTheory.Functor

Functor C D represents a functor between categories C and D.

To apply a functor F to an object use F.obj X, and to a morphism use F.map f.

The axiom map_id expresses preservation of identities, and map_comp expresses functoriality.

structure CategoryTheory.Functor.{v₁, v₂, u₁, u₂} (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C]
  (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : Type (max v₁ v₂ u₁ u₂)

Used by: Component.Impl.toSpecFunctor

`CategoryTheory.Iso`

CategoryTheory.Iso

An isomorphism (a.k.a. an invertible morphism) between two objects of a category. The inverse morphism is bundled.

See also CategoryTheory.Core for the category with the same objects and isomorphisms playing the role of morphisms.

structure CategoryTheory.Iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type v

Used by: Component.Func.braiding, Component.Impl.braiding, Component.Spec.braiding

`CategoryTheory.Monoidal.Braided.Basic`

CategoryTheory.BraidedCategory

A braided monoidal category is a monoidal category equipped with a braiding isomorphism β_ X Y : X ⊗ Y ≅ Y ⊗ X which is natural in both arguments, and also satisfies the two hexagon identities.

structure CategoryTheory.BraidedCategory.{v, u} (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] : Type (max u v)

Used by: Component.Func.braidedCategory, Component.Impl.braidedCategory, Component.Spec.braidedCategory, instBraidedCategoryPROP, instBraidedCategoryPROP_1, instBraidedCategoryPROP_2

`CategoryTheory.Monoidal.Category`

CategoryTheory.MonoidalCategory

In a monoidal category, we can take the tensor product of objects, X ⊗ Y and of morphisms f ⊗ₘ g. Tensor product does not need to be strictly associative on objects, but there is a specified associator, α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z). There is a tensor unit 1_ C, with specified left and right unitor isomorphisms λ_ X : 1_ C ⊗ X ≅ X and ρ_ X : X ⊗ 1_ C ≅ X. These associators and unitors satisfy the pentagon and triangle equations.

structure CategoryTheory.MonoidalCategory.{v, u} (C : Type u) [C : CategoryTheory.Category.{v, u} C] :
  Type (max u v)

Used by: Component.Func.monoidalCategory, Component.Impl.monoidalCategory, Component.Spec.monoidalCategory, instMonoidalCategoryPROP, instMonoidalCategoryPROP_1, instMonoidalCategoryPROP_2

CategoryTheory.MonoidalCategory.ofTensorHom

A constructor for monoidal categories that requires tensorHom instead of whiskerLeft and whiskerRight.

abbrev CategoryTheory.MonoidalCategory.ofTensorHom.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategoryStruct C]
  (id_tensorHom_id :
    ∀ (X₁ X₂ : C),
      CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₁)
          (CategoryTheory.CategoryStruct.id X₂) =
        CategoryTheory.CategoryStruct.id
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) := by
    cat_disch)
  (id_tensorHom :
    ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
      CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) f =
        CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f := by
    cat_disch)
  (tensorHom_id :
    ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
      CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Y) =
        CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y := by
    cat_disch)
  (tensorHom_comp_tensorHom :
    ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
        CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
          (CategoryTheory.CategoryStruct.comp f₂ g₂) := by
    cat_disch)
  (associator_naturality :
    ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
          (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁
            (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃)) := by
    cat_disch)
  (leftUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
            f)
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
          f := by
    cat_disch)
  (rightUnitor_naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f
            (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
          f := by
    cat_disch)
  (pentagon :
    ∀ (W X Y Z : C),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
            (CategoryTheory.CategoryStruct.id Z))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.associator W
                (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
            (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
              (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator
              (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
          (CategoryTheory.MonoidalCategoryStruct.associator W X
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom := by
    cat_disch)
  (triangle :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator X
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
        CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
          (CategoryTheory.CategoryStruct.id Y) := by
    cat_disch) :
  CategoryTheory.MonoidalCategory C

Used by: Component.Func.monoidalCategory, Component.Impl.monoidalCategory, Component.Spec.monoidalCategory

CategoryTheory.MonoidalCategoryStruct

Auxiliary structure to carry only the data fields of (and provide notation for) MonoidalCategory.

structure CategoryTheory.MonoidalCategoryStruct.{v, u} (C : Type u) [C : CategoryTheory.Category.{v, u} C] :
  Type (max u v)

Used by: Component.Func.monoidalCategoryStruct, Component.Impl.monoidalCategoryStruct, Component.Spec.monoidalCategoryStruct

`Data.Fin.Tuple.Basic`

Fin.append

Append a tuple of length m to a tuple of length n to get a tuple of length m + n. This is a non-dependent version of Fin.add_cases.

def Fin.append.{u_1} {m n : ℕ} {α : Sort u_1} (a : Fin m → α) (b : Fin n → α) : Fin (m + n) → α

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.parallel, Component.Func.parallel_sequential, Component.Func.symmetry, Component.Impl.Hom.tensor_id_id, Component.Impl.empty_parallel, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Impl.interchange, Component.Impl.parallel, Component.Impl.parallel_assoc, Component.Impl.parallel_comm, Component.Impl.parallel_congr, Component.Impl.parallel_empty, Component.Impl.symmetry, Component.Impl.symmetry_symmetry, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.parallel_comm, Component.Spec.parallel_sequential, Component.Spec.parallel_toSpec_eq, Component.Spec.symmetry, Component.Spec.symmetry_symmetry, Component.Spec.trace, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_superposing, Component.Spec.trace_vanishing, Component.Spec.trace_yanking, Fin.append_eval, InformationSystem.parallel_delta

Fin.append_assoc

theorem Fin.append_assoc.{u_1} {m n : ℕ} {α : Sort u_1} {p : ℕ} (a : Fin m → α) (b : Fin n → α)
  (c : Fin p → α) : Fin.append (Fin.append a b) c = Fin.append a (Fin.append b c) ∘ Fin.cast ⋯

Used by: Component.Impl.parallel_assoc, Component.Spec.trace_superposing

Fin.append_castAdd_natAdd

theorem Fin.append_castAdd_natAdd.{u_1} {m n : ℕ} {α : Sort u_1} {f : Fin (m + n) → α} :
  (Fin.append (fun i => f (Fin.castAdd n i)) fun i => f (Fin.natAdd m i)) = f

Used by: Component.Impl.Hom.tensor_id_id, Component.Impl.symmetry_symmetry, Component.Spec.parallel_comm, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_superposing

Fin.append_elim0

theorem Fin.append_elim0.{u_1} {m : ℕ} {α : Sort u_1} (u : Fin m → α) :
  Fin.append u Fin.elim0 = u ∘ Fin.cast ⋯

Used by: Component.Impl.parallel_empty, Component.Spec.trace_vanishing

Fin.append_left

theorem Fin.append_left.{u_1} {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin m) :
  Fin.append u v (Fin.castAdd n i) = u i

Used by: Component.Func.parallel_sequential, Component.Impl.interchange, Component.Impl.parallel, Component.Impl.parallel_comm, Component.Impl.symmetry, Component.Impl.symmetry_symmetry, Component.Spec.parallel_comm, Component.Spec.parallel_sequential, Component.Spec.parallel_toSpec_eq, Component.Spec.symmetry_symmetry, Component.Spec.trace_naturality_left, Component.Spec.trace_naturality_right, Component.Spec.trace_sliding, Component.Spec.trace_yanking, Fin.append_eval

Fin.append_left_nil

theorem Fin.append_left_nil.{u_1} {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (hu : m = 0) :
  Fin.append u v = v ∘ Fin.cast ⋯

Used by: Component.Impl.empty_parallel

Fin.append_right

theorem Fin.append_right.{u_1} {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin n) :
  Fin.append u v (Fin.natAdd m i) = v i

`Data.Finset.BooleanAlgebra`

Finset.univ_eq_empty

theorem Finset.univ_eq_empty.{u_1} {α : Type u_1} [Fintype α] [IsEmpty α] : Finset.univ = ∅

Used by: Component.Impl.empty

Finset.univ_nonempty

theorem Finset.univ_nonempty.{u_1} {α : Type u_1} [Fintype α] [Nonempty α] : Finset.univ.Nonempty

Used by: maxWireSize

`Data.Finset.Card`

Finset.card

s.card is the number of elements of s, aka its cardinality.

The notation #s can be accessed in the Finset locale.

def Finset.card.{u_1} {α : Type u_1} (s : Finset α) : ℕ

Used by: BitSequence.trueCount, BitSequence.trueCount_le

Finset.card_filter_le

theorem Finset.card_filter_le.{u_1} {α : Type u_1} (s : Finset α) (p : α → Prop) [DecidablePred p] :
  (Finset.filter p s).card ≤ s.card

Used by: BitSequence.trueCount_le

Finset.card_lt_card

theorem Finset.card_lt_card.{u_1} {α : Type u_1} {s t : Finset α} (h : s ⊂ t) : s.card < t.card

Used by: BitSequence.trueCount_strict

`Data.Finset.Defs`

Finset

Finset α is the type of finite sets of elements of α. It is implemented as a multiset (a list up to permutation) which has no duplicate elements.

structure Finset.{u_4} (α : Type u_4) : Type u_4

Used by: BitSequence.trueCount_strict, Component.Func.toImpl, Component.Impl.empty, Component.Impl.id, Component.Impl.parallel, Component.Impl.symmetry, Discrete.pi, instFintypeCell, instNormNonnegForallFin

Finset.ext_iff

theorem Finset.ext_iff.{u_1} {α : Type u_1} {s₁ s₂ : Finset α} : s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂

Used by: BitSequence.trueCount_strict

`Data.Finset.Filter`

Finset.filter

Finset.filter p s is the set of elements of s that satisfy p.

For example, one can use s.filter (· ∈ t) to get the intersection of s with t : Set α as a Finset α (when a DecidablePred (· ∈ t) instance is available).

def Finset.filter.{u_1} {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset α

Used by: BitSequence.trueCount, BitSequence.trueCount_strict

Finset.mem_filter

theorem Finset.mem_filter.{u_1} {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} {a : α} :
  a ∈ Finset.filter p s ↔ a ∈ s ∧ p a

Used by: BitSequence.trueCount_strict

`Data.Finset.Lattice.Fold`

Finset.sup'

Given nonempty finset s then s.sup' H f is the supremum of its image under f in (possibly unbounded) join-semilattice α, where H is a proof of nonemptiness. If α has a bottom element you may instead use Finset.sup which does not require s nonempty.

def Finset.sup'.{u_2, u_3} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (s : Finset β)
  (H : s.Nonempty) (f : β → α) : α

Used by: maxWireSize

`Data.Fintype.BigOperators`

Fintype.card_fun

theorem Fintype.card_fun.{u_1, u_2} {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] :
  Fintype.card (α → β) = Fintype.card β ^ Fintype.card α

Used by: card_BitFunction, card_BitSequence, phone_number_information

`Data.Fintype.Card`

Finite.injective_iff_surjective

theorem Finite.injective_iff_surjective.{u_1} {α : Type u_1} [Finite α] {f : α → α} :
  Function.Injective f ↔ Function.Surjective f

Used by: Cell.erase_not_surjective

Fintype.card

card α is the number of elements in α, defined when α is a fintype.

def Fintype.card.{u_4} (α : Type u_4) [Fintype α] : ℕ

Used by: InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, card_BitFunction, card_BitFunction_succ_input, card_BitFunction_succ_output, card_BitSequence, phone_number_information, three_doors_information, traffic_light_information

Fintype.card_bool

theorem Fintype.card_bool : Fintype.card Bool = 2

Used by: card_BitSequence

Fintype.card_fin

theorem Fintype.card_fin (n : ℕ) : Fintype.card (Fin n) = n

Used by: BitSequence.trueCount_le, InformationSystem.exists_repeat_state, card_BitSequence, phone_number_information

`Data.Fintype.Defs`

Finset.mem_univ

theorem Finset.mem_univ.{u_1} {α : Type u_1} [Fintype α] (x : α) : x ∈ Finset.univ

Used by: BitSequence.trueCount_strict

Finset.univ

univ is the universal finite set of type Finset α implied from the assumption Fintype α.

def Finset.univ.{u_1} {α : Type u_1} [Fintype α] : Finset α

Used by: BitSequence.trueCount, BitSequence.trueCount_le, BitSequence.trueCount_strict, Component.Func.toImpl, Component.Impl.Simplex.toInformationSystem, Component.Impl.empty, Component.Impl.id, Component.Impl.parallel, Component.Impl.symmetry, Discrete.pi, InformationSystem.parallel_delta, InformationSystem.toSimplex, instFintypeCell, instNormForallFin_computerNetworks, instNormNonnegForallFin, instNormValue, maxWireSize

Fintype

Fintype α means that α is finite, i.e. there are only finitely many distinct elements of type α. The evidence of this is a finset elems (a list up to permutation without duplicates), together with a proof that everything of type α is in the list.

structure Fintype.{u_4} (α : Type u_4) : Type u_4

Used by: BitSequence.trueCount_strict, Channel.capacity, FiniteStateMachine, FiniteStateMachine.Reversible, InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, instFintypeCell, maxWireSize

`Data.Fintype.Pigeonhole`

Fintype.exists_ne_map_eq_of_card_lt

The pigeonhole principle for finitely many pigeons and pigeonholes. This is the Fintype version of Finset.exists_ne_map_eq_of_card_lt_of_maps_to.

theorem Fintype.exists_ne_map_eq_of_card_lt.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β]
  (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y

Used by: InformationSystem.exists_repeat_state

`Data.Int.Cast.Basic`

Int.cast_natCast

theorem Int.cast_natCast.{u} {R : Type u} [AddGroupWithOne R] (n : ℕ) : ↑↑n = ↑n

Used by: irrational_logb_two_three

`Data.Nat.Cast.Defs`

Nat.cast_add

theorem Nat.cast_add.{u_1} {R : Type u_1} [AddMonoidWithOne R] (m n : ℕ) : ↑(m + n) = ↑m + ↑n

Used by: Discrete.prod

Nat.cast_one

theorem Nat.cast_one.{u_1} {R : Type u_1} [AddMonoidWithOne R] : ↑1 = 1

Used by: discrete_Bit, instNormNonnegBit, irrational_logb_two_three

Nat.cast_zero

theorem Nat.cast_zero.{u_1} {R : Type u_1} [AddMonoidWithOne R] : ↑0 = 0

`Data.Nat.Init`

Nat.le_induction

Induction principle starting at a non-zero number. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

This is an alias of Nat.leRec, specialized to Prop.

theorem Nat.le_induction {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop} (base : P m ⋯)
  (succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) (n : ℕ) (hmn : m ≤ n) : P n hmn

Used by: Component.Func.iterate_stays

`Data.Prod.Basic`

Prod.mk.eta

theorem Prod.mk.eta.{u_1, u_2} {α : Type u_1} {β : Type u_2} {p : α × β} : (p.1, p.2) = p

Used by: Component.Impl.recast

`Data.Quot`

Quotient.map

Map a function f : α → β that sends equivalent elements to equivalent elements to a function Quotient sa → Quotient sb. Useful to define unary operations on quotients.

def Quotient.map.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : α → β)
  (h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b) : Quotient sa → Quotient sb

Used by: Component.Impl.Hom.recast

Quotient.map₂

Map a function f : α → β → γ that sends equivalent elements to equivalent elements to a function f : Quotient sa → Quotient sb → Quotient sc. Useful to define binary operations on quotients.

def Quotient.map₂.{u_1, u_2, u_4} {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β}
  {γ : Sort u_4} {sc : Setoid γ} (f : α → β → γ)
  (h : ∀ ⦃a₁ a₂ : α⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂ : β⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
  Quotient sa → Quotient sb → Quotient sc

Used by: Component.Impl.Hom.comp, Component.Impl.Hom.tensor

`Data.Rat.Cast.Defs`

Rat.cast_intCast

theorem Rat.cast_intCast.{u_3} {α : Type u_3} [DivisionRing α] (n : ℤ) : ↑↑n = ↑n

Used by: irrational_logb_two_three

Rat.cast_natCast

theorem Rat.cast_natCast.{u_3} {α : Type u_3} [DivisionRing α] (n : ℕ) : ↑↑n = ↑n

Used by: irrational_logb_two_three

`Data.Rat.Defs`

Rat.pos

theorem Rat.pos (a : ℚ) : 0 < a.den

Used by: irrational_logb_two_three

`Data.Real.Basic`

Real

The type ℝ of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.

structure Real : Type

`Data.Set.Defs`

Set

A set is a collection of elements of some type α.

Although Set is defined as α → Prop, this is an implementation detail which should not be relied on. Instead, setOf and membership of a set (∈) should be used to convert between sets and predicates.

def Set.{u} (α : Type u) : Type u

Used by: irrational_logb_two_three

`Data.Set.Operations`

Set.range

Range of a function.

This function is more flexible than f '' univ, as the image requires that the domain is in Type and not an arbitrary Sort.

def Set.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set α

Used by: irrational_logb_two_three

`Logic.Function.Basic`

Function.invFun

The inverse of a function (which is a left inverse if f is injective and a right inverse if f is surjective).

def Function.invFun.{u, u_3} {α : Sort u} {β : Sort u_3} [Nonempty α] (f : α → β) : β → α

Used by: InformationSystem.reversible

Function.leftInverse_invFun

theorem Function.leftInverse_invFun.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β}
  (hf : Function.Injective f) : Function.LeftInverse (Function.invFun f) f

Used by: InformationSystem.reversible

`Logic.Function.Iterate`

Function.iterate_succ_apply'

theorem Function.iterate_succ_apply'.{u} {α : Type u} (f : α → α) (n : ℕ) (x : α) :
  f^[n.succ] x = f (f^[n] x)

Used by: Component.Func.fixedPoint_isFixed, Component.Func.iterate_dominates_succ, Component.Func.iterate_stays

Nat.iterate

Iterate a function.

def Nat.iterate.{u} {α : Sort u} (op : α → α) : ℕ → α → α

Used by: Component.Func.fixedPoint_isFixed, Component.Func.iterate, Component.Func.iterate_dominates_succ, Component.Func.iterate_stays

`Logic.Nonempty`

Classical.arbitrary

Using Classical.choice, extracts a term from a Nonempty type.

abbrev Classical.arbitrary.{u_3} (α : Sort u_3) [h : Nonempty α] : α

Used by: Component.Spec.not_cartesian, Component.Spec.trace_yanking

`NumberTheory.Real.Irrational`

Irrational

A real number is irrational if it is not equal to any rational number.

def Irrational (x : ℝ) : Prop

Used by: irrational_logb_two_three, traffic_light_information

`Order.Defs.LinearOrder`

le_of_not_gt

theorem le_of_not_gt.{u_1} {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b < a) : a ≤ b

Used by: InformationSystem.Step.bottom, InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

lt_of_not_ge

theorem lt_of_not_ge.{u_1} {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) : a < b

Used by: InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.spontaneous_no_self_return

lt_or_gt_of_ne

theorem lt_or_gt_of_ne.{u_1} {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≠ b) : a < b ∨ b < a

Used by: InformationSystem.exists_repeat_state

lt_trichotomy

theorem lt_trichotomy.{u_1} {α : Type u_1} [LinearOrder α] (a b : α) : a < b ∨ a = b ∨ b < a

Used by: InformationSystem.Step.delta_trichotomy, InformationSystem.eval_trichotomy

`Order.Defs.PartialOrder`

le_refl

The relation ≤ on a preorder is reflexive.

theorem le_refl.{u_1} {α : Type u_1} [Preorder α] (a : α) : a ≤ a

Used by: Component.Func.exists_settle, instNormNonnegBool, instNormNonnegUnit

`Tactic.Linarith.Lemmas`

Mathlib.Tactic.Linarith.add_lt_of_le_of_neg

theorem Mathlib.Tactic.Linarith.add_lt_of_le_of_neg.{u} {α : Type u} [Semiring α] [PartialOrder α]
  [IsStrictOrderedRing α] {a b c : α} (hbc : b ≤ c) (ha : a < 0) : b + a < c

Used by: InformationSystem.Step.bottom, InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

Mathlib.Tactic.Linarith.add_lt_of_neg_of_le

theorem Mathlib.Tactic.Linarith.add_lt_of_neg_of_le.{u} {α : Type u} [Semiring α] [PartialOrder α]
  [IsStrictOrderedRing α] {a b c : α} (ha : a < 0) (hbc : b ≤ c) : a + b < c

Used by: InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.spontaneous_no_self_return

Mathlib.Tactic.Linarith.add_nonpos

theorem Mathlib.Tactic.Linarith.add_nonpos.{u} {α : Type u} [Semiring α] [PartialOrder α] [IsOrderedRing α]
  {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0

Used by: InformationSystem.zero_run_le

Mathlib.Tactic.Linarith.eq_of_eq_of_eq

theorem Mathlib.Tactic.Linarith.eq_of_eq_of_eq.{u_1} {α : Type u_1} [Semiring α] {a b : α} (ha : a = 0)
  (hb : b = 0) : a + b = 0

Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt

theorem Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt.{u_1} {α : Type u_1} [LinearOrder α] (a b : α)
  (h1 : ¬a < b) (h2 : ¬b < a) : a = b

Mathlib.Tactic.Linarith.le_of_eq_of_le

theorem Mathlib.Tactic.Linarith.le_of_eq_of_le.{u} {α : Type u} [Semiring α] [PartialOrder α] {a b : α}
  (ha : a = 0) (hb : b ≤ 0) : a + b ≤ 0

Used by: InformationSystem.Step.bottom, InformationSystem.zero_run_le

Mathlib.Tactic.Linarith.lt_irrefl

theorem Mathlib.Tactic.Linarith.lt_irrefl.{u} {α : Type u} [Preorder α] {a : α} : ¬a < a

Mathlib.Tactic.Linarith.lt_of_eq_of_lt

theorem Mathlib.Tactic.Linarith.lt_of_eq_of_lt.{u} {α : Type u} [Semiring α] [PartialOrder α] {a b : α}
  (ha : a = 0) (hb : b < 0) : a + b < 0

Used by: Component.Impl.Simplex.toInformationSystem, Component.Impl.parallel, Component.Impl.sequential, InformationSystem.Environment.universe, InformationSystem.Step.delta_alt, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.eval_delta, InformationSystem.roundtrip_neutral, InformationSystem.spontaneous_no_self_return, InformationSystem.toSimplex, irrational_logb_two_three

Mathlib.Tactic.Linarith.sub_neg_of_lt

theorem Mathlib.Tactic.Linarith.sub_neg_of_lt.{u} {α : Type u} [Ring α] [PartialOrder α] [IsOrderedRing α]
  {a b : α} : a < b → a - b < 0

Mathlib.Tactic.Linarith.sub_nonpos_of_le

theorem Mathlib.Tactic.Linarith.sub_nonpos_of_le.{u} {α : Type u} [Ring α] [PartialOrder α]
  [IsOrderedRing α] {a b : α} : a ≤ b → a - b ≤ 0

Used by: InformationSystem.Step.bottom, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

`Tactic.NormNum.Basic`

Mathlib.Meta.NormNum.isInt_add

theorem Mathlib.Meta.NormNum.isInt_add.{u_1} {α : Type u_1} [Ring α] {f : α → α → α} {a b : α}
  {a' b' c : ℤ} :
  f = HAdd.hAdd →
    Mathlib.Meta.NormNum.IsInt a a' →
      Mathlib.Meta.NormNum.IsInt b b' → a'.add b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c

Mathlib.Meta.NormNum.isInt_neg

theorem Mathlib.Meta.NormNum.isInt_neg.{u_1} {α : Type u_1} [Ring α] {f : α → α} {a : α} {a' b : ℤ} :
  f = Neg.neg → Mathlib.Meta.NormNum.IsInt a a' → a'.neg = b → Mathlib.Meta.NormNum.IsInt (-a) b

Mathlib.Meta.NormNum.isNat_eq_true

theorem Mathlib.Meta.NormNum.isNat_eq_true.{u} {α : Type u} [AddMonoidWithOne α] {a b : α} {c : ℕ} :
  Mathlib.Meta.NormNum.IsNat a c → Mathlib.Meta.NormNum.IsNat b c → a = b

Used by: discrete_Bit, discrete_Bool, discrete_Unit

Mathlib.Meta.NormNum.isNat_mul

theorem Mathlib.Meta.NormNum.isNat_mul.{u_1} {α : Type u_1} [Semiring α] {f : α → α → α} {a b : α}
  {a' b' c : ℕ} :
  f = HMul.hMul →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.mul b' = c → Mathlib.Meta.NormNum.IsNat (a * b) c

Used by: irrational_logb_two_three

Mathlib.Meta.NormNum.isNat_natCast

theorem Mathlib.Meta.NormNum.isNat_natCast.{u_1} {R : Type u_1} [AddMonoidWithOne R] (n m : ℕ) :
  Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m

Used by: discrete_Bit, discrete_Bool, discrete_Unit

Mathlib.Meta.NormNum.isNat_ofNat

theorem Mathlib.Meta.NormNum.isNat_ofNat.{u} (α : Type u) [AddMonoidWithOne α] {a : α} {n : ℕ}
  (h : ↑n = a) : Mathlib.Meta.NormNum.IsNat a n

`Tactic.NormNum.Eq`

Mathlib.Meta.NormNum.isNat_eq_false

theorem Mathlib.Meta.NormNum.isNat_eq_false.{u_1} {α : Type u_1} [AddMonoidWithOne α] [CharZero α] {a b : α}
  {a' b' : ℕ} :
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.beq b' = false → ¬a = b

Used by: irrational_logb_two_three

`Tactic.NormNum.Ineq`

Mathlib.Meta.NormNum.isNat_le_false

theorem Mathlib.Meta.NormNum.isNat_le_false.{u_1} {α : Type u_1} [Semiring α] [PartialOrder α]
  [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ} (ha : Mathlib.Meta.NormNum.IsNat a a')
  (hb : Mathlib.Meta.NormNum.IsNat b b') (h : a'.ble b' = false) : ¬a ≤ b

Used by: phone_number_information

Mathlib.Meta.NormNum.isNat_le_true

theorem Mathlib.Meta.NormNum.isNat_le_true.{u_1} {α : Type u_1} [Semiring α] [PartialOrder α]
  [IsOrderedRing α] {a b : α} {a' b' : ℕ} :
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.ble b' = true → a ≤ b

Used by: instNormNonnegBit, instNormNonnegCell, irrational_logb_two_three, phone_number_information

Mathlib.Meta.NormNum.isNat_lt_true

theorem Mathlib.Meta.NormNum.isNat_lt_true.{u_1} {α : Type u_1} [Semiring α] [PartialOrder α]
  [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ} :
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.ble a' = false → a < b

Used by: irrational_logb_two_three

`Tactic.NormNum.Pow`

Mathlib.Meta.NormNum.IsNatPowT.bit0

theorem Mathlib.Meta.NormNum.IsNatPowT.bit0 {a b c : ℕ} :
  Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b) (c.mul c)

Used by: phone_number_information

Mathlib.Meta.NormNum.IsNatPowT.bit1

theorem Mathlib.Meta.NormNum.IsNatPowT.bit1 {a b c : ℕ} :
  Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b + 1) (c.mul (c.mul a))

Used by: phone_number_information

Mathlib.Meta.NormNum.IsNatPowT.run

theorem Mathlib.Meta.NormNum.IsNatPowT.run {a b c : ℕ}
  (p : Mathlib.Meta.NormNum.IsNatPowT (a.pow 1 = a) a b c) : a.pow b = c

Used by: phone_number_information

Mathlib.Meta.NormNum.IsNatPowT.trans

This is the key to making the proof proceed as a balanced tree of applications instead of a linear sequence. It is just modus ponens after unwrapping the definitions.

theorem Mathlib.Meta.NormNum.IsNatPowT.trans {a b c : ℕ} {p : Prop} {b' c' : ℕ}
  (h1 : Mathlib.Meta.NormNum.IsNatPowT p a b c)
  (h2 : Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a b' c') :
  Mathlib.Meta.NormNum.IsNatPowT p a b' c'

Used by: phone_number_information

Mathlib.Meta.NormNum.isNat_pow

theorem Mathlib.Meta.NormNum.isNat_pow.{u_1} {α : Type u_1} [Semiring α] {f : α → ℕ → α} {a : α}
  {b a' b' c : ℕ} :
  f = HPow.hPow →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.pow b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c

Used by: phone_number_information

`Tactic.NormNum.Result`

Int.rawCast

A “raw int cast” is an expression of the form:

(Nat.rawCast lit : α) where lit is a raw natural number literal
(Int.rawCast (Int.negOfNat lit) : α) where lit is a nonzero raw natural number literal

(That is, we only actually use this function for negative integers.) This representation is used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

def Int.rawCast.{u} {α : Type u} [Ring α] (n : ℤ) : α

Mathlib.Meta.NormNum.IsInt.of_raw

theorem Mathlib.Meta.NormNum.IsInt.of_raw.{u_1} (α : Type u_1) [Ring α] (n : ℤ) :
  Mathlib.Meta.NormNum.IsInt n.rawCast n

Mathlib.Meta.NormNum.IsInt.to_isNat

theorem Mathlib.Meta.NormNum.IsInt.to_isNat.{u_1} {α : Type u_1} [Ring α] {a : α} {n : ℕ} :
  Mathlib.Meta.NormNum.IsInt a (Int.ofNat n) → Mathlib.Meta.NormNum.IsNat a n

Mathlib.Meta.NormNum.IsInt.to_raw_eq

theorem Mathlib.Meta.NormNum.IsInt.to_raw_eq.{u} {α : Type u} {a : α} {n : ℤ} [Ring α] :
  Mathlib.Meta.NormNum.IsInt a n → a = n.rawCast

Mathlib.Meta.NormNum.IsNat.of_raw

theorem Mathlib.Meta.NormNum.IsNat.of_raw.{u_1} (α : Type u_1) [AddMonoidWithOne α] (n : ℕ) :
  Mathlib.Meta.NormNum.IsNat n.rawCast n

Mathlib.Meta.NormNum.IsNat.to_isInt

theorem Mathlib.Meta.NormNum.IsNat.to_isInt.{u_1} {α : Type u_1} [Ring α] {a : α} {n : ℕ} :
  Mathlib.Meta.NormNum.IsNat a n → Mathlib.Meta.NormNum.IsInt a (Int.ofNat n)

Mathlib.Meta.NormNum.IsNat.to_raw_eq

theorem Mathlib.Meta.NormNum.IsNat.to_raw_eq.{u} {α : Type u} {a : α} {n : ℕ} [AddMonoidWithOne α] :
  Mathlib.Meta.NormNum.IsNat a n → a = n.rawCast

Mathlib.Meta.NormNum.instAddMonoidWithOne

A shortcut (non)instance for AddMonoidWithOne α from Ring α to shrink generated proofs.

def Mathlib.Meta.NormNum.instAddMonoidWithOne.{u} {α : Type u} [Ring α] : AddMonoidWithOne α

Mathlib.Meta.NormNum.instAtLeastTwo

A shortcut (non)instance for Nat.AtLeastTwo (n + 2) to shrink generated proofs.

theorem Mathlib.Meta.NormNum.instAtLeastTwo (n : ℕ) : (n + 2).AtLeastTwo

Used by: instNormNonnegCell, irrational_logb_two_three

Nat.rawCast

A “raw nat cast” is an expression of the form (Nat.rawCast lit : α) where lit is a raw natural number literal. These expressions are used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

def Nat.rawCast.{u} {α : Type u} [AddMonoidWithOne α] (n : ℕ) : α

`Tactic.Push`

Mathlib.Tactic.Push.not_and_eq

theorem Mathlib.Tactic.Push.not_and_eq (p q : Prop) : (¬(p ∧ q)) = (p → ¬q)

Used by: Component.Func.exists_settle

`Tactic.Ring.Basic`

Mathlib.Tactic.Ring.cast_zero

theorem Mathlib.Tactic.Ring.cast_zero.{u_1} {R : Type u_1} [CommSemiring R] {a : R} :
  Mathlib.Meta.NormNum.IsNat a 0 → a = 0

Mathlib.Tactic.Ring.of_eq

theorem Mathlib.Tactic.Ring.of_eq.{u_2} {α : Sort u_2} {a b c : α} : a = c → b = c → a = b

`Tactic.Ring.Common`

Mathlib.Tactic.Ring.Common.add_congr

theorem Mathlib.Tactic.Ring.Common.add_congr.{u_1} {R : Type u_1} [CommSemiring R] {a a' b b' c : R} :
  a = a' → b = b' → a' + b' = c → a + b = c

Mathlib.Tactic.Ring.Common.add_mul

theorem Mathlib.Tactic.Ring.Common.add_mul.{u_1} {R : Type u_1} [CommSemiring R] {a₁ a₂ b c₁ c₂ d : R} :
  a₁ * b = c₁ → a₂ * b = c₂ → c₁ + c₂ = d → (a₁ + a₂) * b = d

Used by: irrational_logb_two_three

Mathlib.Tactic.Ring.Common.add_overlap_pf_zero

theorem Mathlib.Tactic.Ring.Common.add_overlap_pf_zero.{u_1} {R : Type u_1} [CommSemiring R] {a b : R}
  (x : R) (e : ℕ) :
  Mathlib.Meta.NormNum.IsNat (a + b) 0 → Mathlib.Meta.NormNum.IsNat (x ^ e * a + x ^ e * b) 0

Mathlib.Tactic.Ring.Common.add_pf_add_gt

theorem Mathlib.Tactic.Ring.Common.add_pf_add_gt.{u_1} {R : Type u_1} [CommSemiring R] {a b₂ c : R}
  (b₁ : R) : a + b₂ = c → a + (b₁ + b₂) = b₁ + c

Mathlib.Tactic.Ring.Common.add_pf_add_lt

theorem Mathlib.Tactic.Ring.Common.add_pf_add_lt.{u_1} {R : Type u_1} [CommSemiring R] {a₂ b c : R}
  (a₁ : R) : a₂ + b = c → a₁ + a₂ + b = a₁ + c

Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero

theorem Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero.{u_1} {R : Type u_1} [CommSemiring R]
  {a₁ a₂ b₁ b₂ c : R} (h : Mathlib.Meta.NormNum.IsNat (a₁ + b₁) 0) (h₄ : a₂ + b₂ = c) :
  a₁ + a₂ + (b₁ + b₂) = c

Mathlib.Tactic.Ring.Common.add_pf_add_zero

theorem Mathlib.Tactic.Ring.Common.add_pf_add_zero.{u_1} {R : Type u_1} [CommSemiring R] (a : R) : a + 0 = a

Mathlib.Tactic.Ring.Common.add_pf_zero_add

theorem Mathlib.Tactic.Ring.Common.add_pf_zero_add.{u_1} {R : Type u_1} [CommSemiring R] (b : R) : 0 + b = b

Mathlib.Tactic.Ring.Common.atom_pf

theorem Mathlib.Tactic.Ring.Common.atom_pf.{u_1} {R : Type u_1} [CommSemiring R] {b : R} (a : R) {e : ℕ}
  (hone : Nat.rawCast 1 = e) (hb : a ^ e * Nat.rawCast 1 = b) : a = b + 0

Mathlib.Tactic.Ring.Common.mul_add

theorem Mathlib.Tactic.Ring.Common.mul_add.{u_1} {R : Type u_1} [CommSemiring R] {a b₁ b₂ c₁ c₂ d : R} :
  a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d

Used by: irrational_logb_two_three

Mathlib.Tactic.Ring.Common.mul_congr

theorem Mathlib.Tactic.Ring.Common.mul_congr.{u_1} {R : Type u_1} [CommSemiring R] {a a' b b' c : R} :
  a = a' → b = b' → a' * b' = c → a * b = c

Used by: irrational_logb_two_three

Mathlib.Tactic.Ring.Common.mul_pf_left

theorem Mathlib.Tactic.Ring.Common.mul_pf_left.{u_1} {R : Type u_1} [CommSemiring R] {a₃ b c : R} (a₁ : R)
  (a₂ : ℕ) : a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

Used by: irrational_logb_two_three

Mathlib.Tactic.Ring.Common.mul_pf_right

theorem Mathlib.Tactic.Ring.Common.mul_pf_right.{u_1} {R : Type u_1} [CommSemiring R] {a b₃ c : R} (b₁ : R)
  (b₂ : ℕ) : a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Used by: irrational_logb_two_three

Mathlib.Tactic.Ring.Common.mul_zero

theorem Mathlib.Tactic.Ring.Common.mul_zero.{u_1} {R : Type u_1} [CommSemiring R] (a : R) : a * 0 = 0

Used by: irrational_logb_two_three

Mathlib.Tactic.Ring.Common.neg_add

theorem Mathlib.Tactic.Ring.Common.neg_add.{u_2} {R : Type u_2} [CommRing R] {a₁ a₂ b₁ b₂ : R} :
  -a₁ = b₁ → -a₂ = b₂ → -(a₁ + a₂) = b₁ + b₂

Mathlib.Tactic.Ring.Common.neg_congr

theorem Mathlib.Tactic.Ring.Common.neg_congr.{u_2} {R : Type u_2} [CommRing R] {a a' b : R} :
  a = a' → -a' = b → -a = b

Mathlib.Tactic.Ring.Common.neg_mul

theorem Mathlib.Tactic.Ring.Common.neg_mul.{u_2} {R : Type u_2} [CommRing R] (a₁ : R) (a₂ : ℕ) {a₃ b : R} :
  -a₃ = b → -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Mathlib.Tactic.Ring.Common.neg_zero

theorem Mathlib.Tactic.Ring.Common.neg_zero.{u_2} {R : Type u_2} [CommRing R] : -0 = 0

Mathlib.Tactic.Ring.Common.sub_congr

theorem Mathlib.Tactic.Ring.Common.sub_congr.{u_2} {R : Type u_2} [CommRing R] {a a' b b' c : R} :
  a = a' → b = b' → a' - b' = c → a - b = c

Mathlib.Tactic.Ring.Common.sub_pf

theorem Mathlib.Tactic.Ring.Common.sub_pf.{u_2} {R : Type u_2} [CommRing R] {a b c d : R} :
  -b = c → a + c = d → a - b = d

Mathlib.Tactic.Ring.Common.zero_mul

theorem Mathlib.Tactic.Ring.Common.zero_mul.{u_1} {R : Type u_1} [CommSemiring R] (b : R) : 0 * b = 0

Used by: irrational_logb_two_three