jcommelin

❌ le_of_forall_neg_add_le <- ✅ le_of_forall_lt_one_mul_le
❌ le_iff_forall_neg_add_le <- ✅ le_iff_forall_lt_one_mul_le
❌ Sum.FaithfulVAddLeft <- ✅ Sum.FaithfulSMulLeft
❌ nsmul_le_nsmul_iff <- ✅ pow_le_pow_iff'
❌ Multiset.sum_zero <- ✅ Multiset.prod_zero
❌ nsmul_lt_nsmul_iff <- ✅ pow_lt_pow_iff'
❌ Part.left_dom_of_sub_dom <- ✅ Part.left_dom_of_div_dom
❌ Pi.update_eq_sub_add_single <- ✅ Pi.update_eq_div_mul_mulSingle
❌ eq_zero_or_pos <- ✅ eq_one_or_one_lt
❌ WithBot.coe_eq_zero <- ✅ WithBot.coe_eq_one

jcommelin

import demo.structures

/-! # Classes

Define a class (e.g. `monoid`)
and define an instance (e.g. product monoid).

-/

namespace impan

jcommelin

import category_theory.category.basic

open category_theory

/-! # Structures

Define your own structure
(e.g. `prod` or `functor`)
and define examples (e.g. composition).

jcommelin

import category_theory.yoneda
import tactic.apply_fun

.

open category_theory opposite

/-! # Yoneda -/

jcommelin

import category_theory.yoneda
import tactic.apply_fun

.

open category_theory opposite

/-! # Yoneda -/

variables (C : Type) [category.{0} C]

jcommelin

import tactic.find_unused
import challenge

open tactic

meta def file_list : list (option string) :=
["backup/delta_functor.lean", "backup/extr.lean",
"backup/extr_backup.lean", "backup/multilinear.lean",
"backup/prepresentation.lean", "backup/sheafification_mono.lean",
"scripts/lean_version.lean", "scripts/lint_project.lean",

jcommelin

AddCommGroup.Ab.category_theory.limits.has_colimits_of_size
AddCommGroup.colimit_comparison
AddCommGroup.direct_sum_bicone
AddCommGroup.direct_sum_punit_iso
AddCommGroup.hom_product_comparison
AddCommGroup.is_bilimit_direct_sum_bicone
AddCommGroup.is_iso_hom_product_comparison
AddCommGroup.is_limit_pi_fan
AddCommGroup.pi_fan
AddCommGroup.pi_lift

jcommelin

/-
TODO: it's not clear to me (jmc) whether the following items can be easily included,
      maybe they depend on theory of etale algebras, just like the items further below

  ∀ (f : polynomial R) (a₀ : R) (h₁ : f.eval a₀ ∈ maximal_ideal R)
    (h₂ : f.derivative.eval a₀ ∉ maximal_ideal R),
    ∃ a : R, f.is_root a ∧ (a - a₀ ∈ maximal_ideal R),
  ∀ (f : polynomial R) (a₀ : residue_field R) (h₁ : aeval a₀ f = 0)
    (h₂ : aeval a₀ f.derivative ≠ 0),
    ∃ a : R, f.is_root a ∧ (residue R a = a₀),

jcommelin

{ "nodes" : 

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_ssubset",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 340 }

jcommelin

{ "nodes" : 

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_coe_t_aux",
"topic" : "core",
"file" : "core/init/coe.lean",
"line" : 123 }