b-mehta

-- pairs below 10^9
0,1
8,1
20,25
30,25
88,209
494,209
494,1729
6048,1729
744,1984

b-mehta

\documentclass{article}
\usepackage{tikz}
\usepackage[landscape]{geometry}
\usetikzlibrary{backgrounds}

\begin{document}
\begin{center}
    \begin{tikzpicture}[scale=2]
        \begin{scope}[every path/.append style={gray, ultra thin}]
            \fill [orange!10] (2, 1) rectangle (6, 2);

b-mehta

\documentclass{article}
\usepackage{tikz}
\begin{document}
\begin{center}
  \begin{tikzpicture}[scale=0.7]
    \begin{scope}
      \draw (-1,0) to[bend left=40] (1,0);
      \draw (-1.2,0.15) to[bend right=40] (1.2,0.15);
      \draw ( 3,0) to[bend left=40] (5,0);
      \draw ( 2.8,0.15) to[bend right=40] (5.2,0.15);

b-mehta

test :: [a] -> Bool
test (_:_:_) = True
test _ = False

b-mehta

b-mehta

[type_context.is_def_eq_detail] [1]: Ω C ⟶ Ω C =?= Ω C ⟶ Ω C
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω C
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_ C
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω C

b-mehta

import category_theory.monad.algebra
import data.sigma

namespace category_theory

open category_theory category_theory.category category_theory.limits comonad

universes v u

variables {C : Type u} [small_category C]

b-mehta

 Freeze display
Tactic State
1 goal
α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_inverse_obj : β → α,
e_inverse_map : Π {X Y : β}, (X ⟶ Y) → (e_inverse_obj X ⟶ e_inverse_obj Y),
e_inverse_map_id' :

b-mehta

 Freeze display
Tactic State
4 goals
α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_functor : α ⥤ β,
e_inverse : β ⥤ α,
e_unit_iso : 𝟭 α ≅ e_functor ⋙ e_inverse,

b-mehta

import data.finset
import category_theory.category
import category_theory.isomorphism

namespace category_theory
open set category_theory.category

universes v u

/-- A partition of the type s into finitely many bits -/