should build? #155
Annotations
10 warnings and 10 notices
src/hints/category_theory/exercise1/hint1.lean#L9
/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise1/hint1.lean:9:0:
declaration 'iso_of_hom_iso_attempt_1' uses sorry
|
src/hints/category_theory/exercise2/hint1.lean#L13
/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint1.lean:13:0:
declaration 'CommRing.polynomial' uses sorry
|
src/hints/category_theory/exercise2/hint3.lean#L35
/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint3.lean:35:0:
declaration 'CommRing.polynomial' uses sorry
|
src/hints/category_theory/exercise2/hint2.lean#L21
/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint2.lean:21:0:
declaration 'CommRing.polynomial' uses sorry
|
src/exercises_sources/thursday/category_theory/exercise2.lean#L15
/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/thursday/category_theory/exercise2.lean:15:0:
declaration 'Ring.polynomial' uses sorry
|
src/hints/category_theory/exercise2/hint5.lean#L12
/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint5.lean:12:0:
declaration 'CommRing.polynomial' uses sorry
|
src/exercises_sources/thursday/category_theory/exercise2.lean#L18
/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/thursday/category_theory/exercise2.lean:18:0:
declaration 'CommRing.polynomial' uses sorry
|
src/exercises_sources/monday/metaprogramming.lean#L41
/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/monday/metaprogramming.lean:41:0:
declaration '[anonymous]' uses sorry
|
src/hints/category_theory/exercise2/hint1.lean#L18
/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint1.lean:18:0:
declaration 'commutes' uses sorry
|
src/hints/category_theory/exercise2/hint3.lean#L40
/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint3.lean:40:0:
declaration 'commutes' uses sorry
|
src/demos/linalg.lean#L23
/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:23:0:
@[_ext_core id.{1} name module.ext, class, ext option.none.{0} name, protect_proj list.nil.{0} name]
structure module : Π (R : Type u) (M : Type v) [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M], Type (max u v)
fields:
module.to_distrib_mul_action : Π {R : Type u} {M : Type v} [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M] [self : module R M],
distrib_mul_action R M
module.add_smul : ∀ {R : Type u} {M : Type v} [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M] [self : module R M] (r s : R)
(x : M), (r + s) • x = r • x + s • x
module.zero_smul : ∀ {R : Type u} {M : Type v} [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M] [self : module R M] (x : M),
0 • x = 0
|
src/demos/linalg.lean#L32
/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:32:0:
add_smul : ∀ (r s : ?M_1) (x : ?M_2), (r + s) • x = r • x + s • x
|
src/demos/linalg.lean#L33
/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:33:0:
smul_add : ∀ (a : ?M_1) (b₁ b₂ : ?M_2), a • (b₁ + b₂) = a • b₁ + a • b₂
|
src/demos/linalg.lean#L34
/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:34:0:
mul_smul : ∀ (x y : ?M_1) (b : ?M_2), (x * y) • b = x • y • b
|
src/demos/linalg.lean#L35
/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:35:0:
one_smul : ∀ (M : Type u_1) {α : Type u_2} [_inst_1 : monoid M] [_inst_2 : mul_action M α] (b : α), 1 • b = b
|
src/demos/linalg.lean#L36
/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:36:0:
zero_smul :
∀ (R : Type u_1) {M : Type u_2} [_inst_1 : has_zero R] [_inst_2 : has_zero M] [_inst_3 : smul_with_zero R M]
(m : M), 0 • m = 0
|
src/solutions/friday/topology.lean#L97
/home/runner/work/lftcm2020/lftcm2020/src/solutions/friday/topology.lean:97:0:
sets_of_superset :
∀ {α : Type u_1} (self : filter α) {x y : set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets
|
src/solutions/thursday/category_theory/exercise4.lean#L27
/home/runner/work/lftcm2020/lftcm2020/src/solutions/thursday/category_theory/exercise4.lean:27:3:
Try this: exact algebra_map ℤ ↥R
|
src/demos/linalg.lean#L37
/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:37:0:
smul_zero : ∀ (a : ?M_1), a • 0 = 0
|
src/exercises_sources/friday/topology.lean#L56
/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/friday/topology.lean:56:0:
sets_of_superset :
∀ {α : Type u_1} (self : filter α) {x y : set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets
|
The logs for this run have expired and are no longer available.
Loading