Dataset Preview
The full dataset viewer is not available (click to read why). Only showing a preview of the rows.
The dataset generation failed
Error code: DatasetGenerationError
Exception: ArrowNotImplementedError
Message: extension
Traceback: Traceback (most recent call last):
File "/usr/local/lib/python3.12/site-packages/datasets/builder.py", line 1893, in _prepare_split_single
writer.write_table(table)
File "/usr/local/lib/python3.12/site-packages/datasets/arrow_writer.py", line 765, in write_table
self._write_table(pa_table, writer_batch_size=writer_batch_size)
File "/usr/local/lib/python3.12/site-packages/datasets/arrow_writer.py", line 773, in _write_table
pa_table = table_cast(pa_table, self._schema)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.12/site-packages/datasets/table.py", line 2281, in table_cast
return cast_table_to_schema(table, schema)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.12/site-packages/datasets/table.py", line 2234, in cast_table_to_schema
table[name] if name in table_column_names else pa.array([None] * len(table), type=schema.field(name).type),
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "pyarrow/array.pxi", line 375, in pyarrow.lib.array
File "pyarrow/array.pxi", line 46, in pyarrow.lib._sequence_to_array
File "pyarrow/error.pxi", line 155, in pyarrow.lib.pyarrow_internal_check_status
File "pyarrow/error.pxi", line 92, in pyarrow.lib.check_status
pyarrow.lib.ArrowNotImplementedError: extension
The above exception was the direct cause of the following exception:
Traceback (most recent call last):
File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 1342, in compute_config_parquet_and_info_response
parquet_operations, partial, estimated_dataset_info = stream_convert_to_parquet(
^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 907, in stream_convert_to_parquet
builder._prepare_split(split_generator=splits_generators[split], file_format="parquet")
File "/usr/local/lib/python3.12/site-packages/datasets/builder.py", line 1739, in _prepare_split
for job_id, done, content in self._prepare_split_single(
^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/usr/local/lib/python3.12/site-packages/datasets/builder.py", line 1925, in _prepare_split_single
raise DatasetGenerationError("An error occurred while generating the dataset") from e
datasets.exceptions.DatasetGenerationError: An error occurred while generating the datasetNeed help to make the dataset viewer work? Make sure to review how to configure the dataset viewer, and open a discussion for direct support.
isProp bool | kind string | name list | typeFallback string | typeFull string | typeReadable string | typeReferences list | valueReferences list |
|---|---|---|---|---|---|---|---|
true | theorem | [
"\"AddConstMap\"",
"\"mkFract\"",
"\"_proof_2\""
] | forall {R : Type.{u_1}} {G : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Ring.{u_1} R] [[email protected]._hygCtx._hyg.7 : LinearOrder.{u_1} R] [[email protected]._hygCtx._hyg.10 : IsStrictOrderedRing.{u_1} R (R... | ∀ {R : Type u_1} {G : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R]
[inst_3 : FloorRing R] [inst_4 : AddGroup G] (a : G) (x : ↑(Set.Ico 0 1) → G),
(fun f x => f ↑x) ((fun f => { toFun := fun x => f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x) = x | ∀ {R : Type u_1} {G : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R]
[inst_3 : FloorRing R] [inst_4 : AddGroup G] (a : G) (x : ↑(Set.Ico 0 1) → G),
(fun f x => f ↑x) ((fun f => { toFun := fun x => f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x) = x | [
[
"Ring",
"toNonAssocRing"
],
[
"PartialOrder",
"toPreorder"
],
[
"Membership",
"mem"
],
[
"Preorder",
"toLT"
],
[
"AddGroupWithOne",
"toAddMonoidWithOne"
],
[
"Subtype",
"val"
],
[
"Set",
"Elem"
],
[
"NonUnitalNonAssocRing",
... | [
[
"\"Int\"",
"\"instCommRing\""
],
[
"\"SubtractionMonoid\"",
"\"toSubNegZeroMonoid\""
],
[
"\"Ring\"",
"\"toNonAssocRing\""
],
[
"\"PartialOrder\"",
"\"toPreorder\""
],
[
"\"Eq\"",
"\"trans\""
],
[
"\"Membership\"",
"\"mem\""
],
[
"\"Preor... |
false | definition | [
"\"AddConstMap\"",
"\"ctorIdx\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} {[email protected]._hygCtx._hyg.4 : Add.{u_1} G} {[email protected]._hygCtx._hyg.7 : Add.{u_2} H} {a : G} {b : H}, (AddConstMap.{u_1, u_2} G H [email protected]._hygCtx._hyg.... | {G : Type u_1} → {H : Type u_2} → {inst : Add G} → {inst_1 : Add H} → {a : G} → {b : H} → AddConstMap G H a b → ℕ | {G : Type u_1} → {H : Type u_2} → {inst : Add G} → {inst_1 : Add H} → {a : G} → {b : H} → AddConstMap G H a b → ℕ | [
[
"Nat"
],
[
"AddConstMap"
],
[
"Add"
]
] | [] |
true | theorem | [
"\"AddConstMap\"",
"\"mk\"",
"\"inj\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} {[email protected]._hygCtx._hyg.4 : Add.{u_1} G} {[email protected]._hygCtx._hyg.7 : Add.{u_2} H} {a : G} {b : H} {toFun : G -> H} {map_add_const' : forall (x : G), Eq.{succ u_2} H (toFun (HAdd.hAdd.{u_1, u_1,... | ∀ {G : Type u_1} {H : Type u_2} {inst : Add G} {inst_1 : Add H} {a : G} {b : H} {toFun : G → H}
{map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b} {toFun_1 : G → H}
{map_add_const'_1 : ∀ (x : G), toFun_1 (x + a) = toFun_1 x + b},
{ toFun := toFun, map_add_const' := map_add_const' } = { toFun := toFun_1, ma... | ∀ {G : Type u_1} {H : Type u_2} {inst : Add G} {inst_1 : Add H} {a : G} {b : H} {toFun : G → H}
{map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b} {toFun_1 : G → H}
{map_add_const'_1 : ∀ (x : G), toFun_1 (x + a) = toFun_1 x + b},
{ toFun := toFun, map_add_const' := map_add_const' } = { toFun := toFun_1, ma... | [
[
"HAdd",
"hAdd"
],
[
"AddConstMap",
"mk"
],
[
"AddConstMap"
],
[
"instHAdd"
],
[
"Add"
],
[
"Eq"
]
] | [
[
"\"eq_of_heq\""
],
[
"\"Eq\""
],
[
"\"AddConstMap\"",
"\"mk\"",
"\"noConfusion\""
]
] |
false | definition | [
"\"AddConstMap\"",
"\"instFunLike\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H}, FunLike.{max (succ u_2) (succ u_1), succ u_1, succ u_2} (AddConstMap.{u_1, u_2} G H [email protected]... | {G : Type u_1} →
{H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → FunLike (AddConstMap G H a b) G H | {G : Type u_1} →
{H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → FunLike (AddConstMap G H a b) G H | [
[
"FunLike"
],
[
"AddConstMap"
],
[
"Add"
]
] | [
[
"\"DFunLike\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"toFun\""
],
[
"\"AddConstMap\"",
"\"instFunLike\"",
"\"_proof_1\""
]
] |
false | definition | [
"\"AddConstMap\"",
"\"instVAddOfVAddAssocClass\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} {K : Type.{u_3}} [[email protected]._hygCtx._hyg.13 : VAdd.{u_3... | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} → {b : H} → {K : Type u_3} → [inst_2 : VAdd K H] → [VAddAssocClass K H H] → VAdd K (AddConstMap G H a b) | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} → {b : H} → {K : Type u_3} → [inst_2 : VAdd K H] → [VAddAssocClass K H H] → VAdd K (AddConstMap G H a b) | [
[
"VAdd"
],
[
"AddConstMap"
],
[
"Add"
],
[
"Add",
"toVAdd"
],
[
"VAddAssocClass"
]
] | [
[
"\"instHVAdd\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"instVAddOfVAddAssocClass\"",
"\"_proof_1\""
],
[
"\"Function\"",
"\"hasVAdd\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"in... |
false | definition | [
"\"AddConstMap\"",
"\"instMul\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, Mul.{u_1} (AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) | {G : Type u_1} → [inst : Add G] → {a : G} → Mul (AddConstMap G G a a) | {G : Type u_1} → [inst : Add G] → {a : G} → Mul (AddConstMap G G a a) | [
[
"AddConstMap"
],
[
"Add"
],
[
"Mul"
]
] | [
[
"\"Mul\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"comp\""
]
] |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_add_nsmul\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {a : G} {b : H} [[email protected]._hygCtx._hyg.12 : AddMonoid.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddMonoid G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x + n • a) = f x + n • b | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddMonoid G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x + n • a) = f x + n • b | [
[
"FunLike"
],
[
"instHAdd"
],
[
"AddMonoid"
],
[
"AddConstMapClass"
],
[
"DFunLike",
"coe"
],
[
"HAdd",
"hAdd"
],
[
"Nat"
],
[
"AddMonoid",
"toNSMul"
],
[
"AddMonoid",
"toAddSemigroup"
],
[
"HSMul",
"hSMul"
],
[
... | [
[
"\"Function\"",
"\"Semiconj\"",
"\"iterate_right\""
],
[
"\"Eq\"",
"\"mp\""
],
[
"\"instHAdd\""
],
[
"\"AddConstMapClass\"",
"\"semiconj\""
],
[
"\"add_right_iterate\""
],
[
"\"AddZero\"",
"\"toAdd\""
],
[
"\"AddZeroClass\"",
"\"toAddZero... |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_sub_int\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] [[email protected]._hygCtx._hyg.12 : AddGroupWithOne.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddGroupWithOne G]
[inst_2 : AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ), f (x - ↑n) = f x - ↑n | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddGroupWithOne G]
[inst_2 : AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ), f (x - ↑n) = f x - ↑n | [
[
"FunLike"
],
[
"AddGroupWithOne",
"toAddMonoidWithOne"
],
[
"AddGroupWithOne"
],
[
"AddConstMapClass"
],
[
"AddMonoidWithOne",
"toAddMonoid"
],
[
"Int",
"cast"
],
[
"DFunLike",
"coe"
],
[
"OfNat",
"ofNat"
],
[
"Int"
],
[
... | [
[
"\"Eq\"",
"\"trans\""
],
[
"\"AddGroupWithOne\"",
"\"toAddMonoidWithOne\""
],
[
"\"Int\"",
"\"cast\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"congrArg\""
],
[
"\"AddConstMapClass\"",
"\"map_sub_int'\""
],
[
"\"zsmul_one\""
],
[
"\"SubN... |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_add_one\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {b : H} [[email protected]._hygCtx._hyg.12 : AddMonoidWithOne.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
[inst_2 : Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G), f (x + 1) = f x + b | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
[inst_2 : Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G), f (x + 1) = f x + b | [
[
"FunLike"
],
[
"instHAdd"
],
[
"Add"
],
[
"AddConstMapClass"
],
[
"AddMonoidWithOne",
"toAddMonoid"
],
[
"DFunLike",
"coe"
],
[
"OfNat",
"ofNat"
],
[
"HAdd",
"hAdd"
],
[
"One",
"toOfNat1"
],
[
"AddMonoid",
"toAddSe... | [
[
"\"AddConstMapClass\"",
"\"map_add_const\""
],
[
"\"One\"",
"\"toOfNat1\""
],
[
"\"AddMonoid\"",
"\"toAddSemigroup\""
],
[
"\"AddMonoidWithOne\"",
"\"toOne\""
],
[
"\"AddMonoidWithOne\"",
"\"toAddMonoid\""
],
[
"\"OfNat\"",
"\"ofNat\""
],
[
... |
true | theorem | [
"\"AddConstMap\"",
"\"instVAddOfVAddAssocClass\"",
"\"_proof_1\""
] | forall {G : Type.{u_3}} {H : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_3} G] [[email protected]._hygCtx._hyg.7 : Add.{u_1} H] {a : G} {b : H} {K : Type.{u_2}} [[email protected]._hygCtx._hyg.13 : VAdd.{u_2... | ∀ {G : Type u_3} {H : Type u_1} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {K : Type u_2} [inst_2 : VAdd K H]
[VAddAssocClass K H H] (c : K) (f : AddConstMap G H a b) (x : G), (c +ᵥ ⇑f) (x + a) = (c +ᵥ ⇑f) x + b | ∀ {G : Type u_3} {H : Type u_1} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {K : Type u_2} [inst_2 : VAdd K H]
[VAddAssocClass K H H] (c : K) (f : AddConstMap G H a b) (x : G), (c +ᵥ ⇑f) (x + a) = (c +ᵥ ⇑f) x + b | [
[
"VAdd"
],
[
"AddConstMap"
],
[
"instHVAdd"
],
[
"Add"
],
[
"instHAdd"
],
[
"Function",
"hasVAdd"
],
[
"DFunLike",
"coe"
],
[
"HVAdd",
"hVAdd"
],
[
"AddConstMap",
"instFunLike"
],
[
"VAddAssocClass"
],
[
"HAdd",
... | [
[
"\"AddConstMapClass\"",
"\"map_add_const\""
],
[
"\"instHVAdd\""
],
[
"\"AddConstMap\""
],
[
"\"Eq\"",
"\"trans\""
],
[
"\"True\""
],
[
"\"instHAdd\""
],
[
"\"outParam\""
],
[
"\"vadd_add_assoc\""
],
[
"\"Function\"",
"\"hasVAdd\""
... |
true | theorem | [
"\"AddConstMap\"",
"\"instMonoid\"",
"\"_proof_4\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G} ([email protected]._hygCtx._hyg.38 : AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]... | ∀ {G : Type u_1} [inst : Add G] {a : G} (x : AddConstMap G G a a) (x_1 : ℕ), ⇑(x ^ x_1) = ⇑(x ^ x_1) | ∀ {G : Type u_1} [inst : Add G] {a : G} (x : AddConstMap G G a a) (x_1 : ℕ), ⇑(x ^ x_1) = ⇑(x ^ x_1) | [
[
"instHPow"
],
[
"Nat"
],
[
"AddConstMap"
],
[
"Add"
],
[
"AddConstMap",
"instPowNat"
],
[
"Function",
"End"
],
[
"HPow",
"hPow"
],
[
"Eq"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
]
] | [
[
"\"instHPow\""
],
[
"\"rfl\""
],
[
"\"Nat\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"instPowNat\""
],
[
"\"Function\"",
"\"End\""
],
[
"\"HPow\"",
"\"hPow\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"... |
false | definition | [
"\"AddConstMap\"",
"\"id\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a | {G : Type u_1} → [inst : Add G] → {a : G} → AddConstMap G G a a | {G : Type u_1} → [inst : Add G] → {a : G} → AddConstMap G G a a | [
[
"AddConstMap"
],
[
"Add"
]
] | [
[
"\"AddConstMap\"",
"\"id\"",
"\"_proof_1\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"id\""
]
] |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_sub_one\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {b : H} [[email protected]._hygCtx._hyg.12 : AddGroup.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddGroup G] [inst_2 : One G]
[inst_3 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G), f (x - 1) = f x - b | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddGroup G] [inst_2 : One G]
[inst_3 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G), f (x - 1) = f x - b | [
[
"FunLike"
],
[
"AddConstMapClass"
],
[
"DFunLike",
"coe"
],
[
"OfNat",
"ofNat"
],
[
"SubNegMonoid",
"toAddMonoid"
],
[
"One",
"toOfNat1"
],
[
"SubNegMonoid",
"toSub"
],
[
"AddMonoid",
"toAddSemigroup"
],
[
"One"
],
[
... | [
[
"\"One\"",
"\"toOfNat1\""
],
[
"\"AddConstMapClass\"",
"\"map_sub_const\""
],
[
"\"OfNat\"",
"\"ofNat\""
]
] |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_sub_nsmul\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {a : G} {b : H} [[email protected]._hygCtx._hyg.12 : AddGroup.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
[inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x - n • a) = f x - n • b | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
[inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x - n • a) = f x - n • b | [
[
"FunLike"
],
[
"AddConstMapClass"
],
[
"DFunLike",
"coe"
],
[
"Nat"
],
[
"AddMonoid",
"toNSMul"
],
[
"SubNegMonoid",
"toAddMonoid"
],
[
"AddMonoid",
"toAddSemigroup"
],
[
"SubNegMonoid",
"toSub"
],
[
"HSMul",
"hSMul"
],
... | [
[
"\"Eq\"",
"\"trans\""
],
[
"\"sub_add_cancel\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"congrArg\""
],
[
"\"SubNegMonoid\"",
"\"toSub\""
],
[
"\"AddConstMapClass\"",
"\"map_add_nsmul\""
],
[
"\"HSub\"",
"\"hSub\""
],
[
"\"Eq\"",
"\... |
true | theorem | [
"\"AddConstMap\"",
"\"one_def\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, Eq.{succ u_1} (AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) (OfNat.ofNat.{u_1} (... | ∀ {G : Type u_1} [inst : Add G] {a : G}, 1 = AddConstMap.id | ∀ {G : Type u_1} [inst : Add G] {a : G}, 1 = AddConstMap.id | [
[
"One",
"toOfNat1"
],
[
"AddConstMap"
],
[
"Add"
],
[
"AddConstMap",
"instOne"
],
[
"Eq"
],
[
"AddConstMap",
"id"
],
[
"OfNat",
"ofNat"
]
] | [
[
"\"rfl\""
],
[
"\"One\"",
"\"toOfNat1\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"instOne\""
],
[
"\"OfNat\"",
"\"ofNat\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"instMonoid\"",
"\"_proof_3\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G} ([email protected]._hygCtx._hyg.31 : AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]... | ∀ {G : Type u_1} [inst : Add G] {a : G} (x x_1 : AddConstMap G G a a), ⇑(x * x_1) = ⇑(x * x_1) | ∀ {G : Type u_1} [inst : Add G] {a : G} (x x_1 : AddConstMap G G a a), ⇑(x * x_1) = ⇑(x * x_1) | [
[
"AddConstMap"
],
[
"Add"
],
[
"instHMul"
],
[
"HMul",
"hMul"
],
[
"AddConstMap",
"instMul"
],
[
"Function",
"End"
],
[
"Eq"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
]
] | [
[
"\"rfl\""
],
[
"\"AddConstMap\""
],
[
"\"instHMul\""
],
[
"\"HMul\"",
"\"hMul\""
],
[
"\"AddConstMap\"",
"\"instMul\""
],
[
"\"Function\"",
"\"End\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
]
] |
false | definition | [
"\"AddConstMap\"",
"\"toEnd\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, MonoidHom.{u_1, u_1} (AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) (Function.End.{u... | {G : Type u_1} → [inst : Add G] → {a : G} → AddConstMap G G a a →* Function.End G | {G : Type u_1} → [inst : Add G] → {a : G} → AddConstMap G G a a →* Function.End G | [
[
"MulOneClass",
"toMulOne"
],
[
"AddConstMap",
"instMonoid"
],
[
"AddConstMap"
],
[
"Add"
],
[
"Monoid",
"toMulOneClass"
],
[
"MonoidHom"
],
[
"Function",
"End"
],
[
"instMonoidEnd"
]
] | [
[
"\"MulOneClass\"",
"\"toMulOne\""
],
[
"\"MonoidHom\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"MulOne\"",
"\"toOne\""
],
[
"\"AddConstMap\"",
"\"toEnd\"",
"\"_proof_2\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instF... |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_nsmul_add\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {a : G} {b : H} [[email protected]._hygCtx._hyg.12 : AddCommMonoid.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommMonoid G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ℕ) (x : G), f (n • a + x) = f x + n • b | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommMonoid G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ℕ) (x : G), f (n • a + x) = f x + n • b | [
[
"FunLike"
],
[
"instHAdd"
],
[
"AddMonoid"
],
[
"AddCommMonoid",
"toAddMonoid"
],
[
"AddConstMapClass"
],
[
"DFunLike",
"coe"
],
[
"HAdd",
"hAdd"
],
[
"AddCommMonoid"
],
[
"Nat"
],
[
"AddMonoid",
"toNSMul"
],
[
"Ad... | [
[
"\"instHAdd\""
],
[
"\"AddCommMonoid\"",
"\"toAddMonoid\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"congrArg\""
],
[
"\"HAdd\"",
"\"hAdd\""
],
[
"\"Nat\""
],
[
"\"AddCommMonoid\"",
"\"toAddCommSemigroup\""
],
[
"\"AddMonoid\"",
"\"toNSM... |
false | definition | [
"\"AddConstMap\"",
"\"instMonoid\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, Monoid.{u_1} (AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) | {G : Type u_1} → [inst : Add G] → {a : G} → Monoid (AddConstMap G G a a) | {G : Type u_1} → [inst : Add G] → {a : G} → Monoid (AddConstMap G G a a) | [
[
"AddConstMap"
],
[
"Add"
],
[
"Monoid"
]
] | [
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"instMonoid\"",
"\"_proof_2\""
],
[
"\"AddConstMap\"",
"\"instPowNat\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instMonoid\"",
"\"_proof_3\""
],
[
"\"AddConstMap\"",
"\"instFunLike... |
false | definition | [
"\"AddConstMap\"",
"\"recOn\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} {motive : (AddConstMap.{u_1, u_2} G H [email protected]._hyg... | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} →
{b : H} →
{motive : AddConstMap G H a b → Sort u} →
(t : AddConstMap G H a b) →
((toFun : G → H) →
(map_add_const' : ∀ (x : G), toFun (x + a) = toFu... | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} →
{b : H} →
{motive : AddConstMap G H a b → Sort u} →
(t : AddConstMap G H a b) →
((toFun : G → H) →
(map_add_const' : ∀ (x : G), toFun (x + a) = toFu... | [
[
"HAdd",
"hAdd"
],
[
"AddConstMap",
"mk"
],
[
"AddConstMap"
],
[
"instHAdd"
],
[
"Add"
],
[
"Eq"
]
] | [
[
"\"AddConstMap\"",
"\"rec\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"instAddConstMapClass\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H}, AddConstMapClass.{max u_2 u_1, u_1, u_2} (AddConstMap.{u_1, u_2} G H [email protected]... | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H},
AddConstMapClass (AddConstMap G H a b) G H a b | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H},
AddConstMapClass (AddConstMap G H a b) G H a b | [
[
"AddConstMap"
],
[
"Add"
],
[
"AddConstMapClass"
],
[
"AddConstMap",
"instFunLike"
]
] | [
[
"\"AddConstMapClass\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"map_add_const'\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
]
] |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_one\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {b : H} [[email protected]._hygCtx._hyg.12 : AddZeroClass.{u_2} G] [[email protected].... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddZeroClass G] [inst_2 : One G]
[inst_3 : Add H] [AddConstMapClass F G H 1 b] (f : F), f 1 = f 0 + b | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddZeroClass G] [inst_2 : One G]
[inst_3 : Add H] [AddConstMapClass F G H 1 b] (f : F), f 1 = f 0 + b | [
[
"FunLike"
],
[
"AddZeroClass"
],
[
"Add"
],
[
"instHAdd"
],
[
"AddConstMapClass"
],
[
"AddZero",
"toAdd"
],
[
"AddZeroClass",
"toAddZero"
],
[
"DFunLike",
"coe"
],
[
"OfNat",
"ofNat"
],
[
"HAdd",
"hAdd"
],
[
"O... | [
[
"\"AddConstMapClass\"",
"\"map_const\""
],
[
"\"One\"",
"\"toOfNat1\""
],
[
"\"OfNat\"",
"\"ofNat\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"toEnd_apply\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, Eq.{succ u_1} ((AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) -> G -> G) (DFunLike.c... | ∀ {G : Type u_1} [inst : Add G] {a : G}, ⇑AddConstMap.toEnd = DFunLike.coe | ∀ {G : Type u_1} [inst : Add G] {a : G}, ⇑AddConstMap.toEnd = DFunLike.coe | [
[
"MulOneClass",
"toMulOne"
],
[
"AddConstMap"
],
[
"Add"
],
[
"MonoidHom"
],
[
"AddConstMap",
"toEnd"
],
[
"MonoidHom",
"instFunLike"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
],
[
"AddConstMap",
"instMonoid"... | [
[
"\"MulOneClass\"",
"\"toMulOne\""
],
[
"\"AddConstMap\"",
"\"instMonoid\""
],
[
"\"AddConstMap\""
],
[
"\"Eq\"",
"\"refl\""
],
[
"\"AddConstMap\"",
"\"toEnd\""
],
[
"\"Monoid\"",
"\"toMulOneClass\""
],
[
"\"MonoidHom\""
],
[
"\"Monoid... |
true | theorem | [
"\"AddConstMap\"",
"\"instAddActionOfVAddAssocClass\"",
"\"_proof_1\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H}, Function.Injective.{succ (max u_1 u_2), max (succ u_1) (succ u_2)} (AddConstMap.{u_1, u_2} G H... | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H}, Function.Injective fun f => ⇑f | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H}, Function.Injective fun f => ⇑f | [
[
"AddConstMap"
],
[
"Add"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
],
[
"Function",
"Injective"
]
] | [
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
],
[
"\"DFunLike\"",
"\"coe_injective\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"coe_addLeftHom_apply\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.3 : AddMonoid.{u_1} G] {a : G} (c : Multiplicative.{u_1} G), Eq.{succ u_1} (G -> G) (DFunLike.coe.{succ u_1, succ u_1, succ u_1} (AddConstMap.{u_1, u_1} G G (AddSemigroup.toAdd.{u_1} G (AddMonoid.toAddSemigroup.{u_1} G [email protected]... | ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} (c : Multiplicative G),
⇑(AddConstMap.addLeftHom c) = Multiplicative.toAdd c +ᵥ id | ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} (c : Multiplicative G),
⇑(AddConstMap.addLeftHom c) = Multiplicative.toAdd c +ᵥ id | [
[
"MulOneClass",
"toMulOne"
],
[
"Multiplicative",
"toAdd"
],
[
"Equiv",
"instEquivLike"
],
[
"MonoidHom"
],
[
"MonoidHom",
"instFunLike"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
],
[
"Equiv"
],
[
"AddAction"... | [
[
"\"MulOneClass\"",
"\"toMulOne\""
],
[
"\"AddConstMap\""
],
[
"\"MonoidHom\""
],
[
"\"MonoidHom\"",
"\"instFunLike\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
],
[
"\"AddConstMap\"",
"\"addLeftHom\""
],
[
... |
false | definition | [
"\"AddConstMap\"",
"\"instOne\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, One.{u_1} (AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) | {G : Type u_1} → [inst : Add G] → {a : G} → One (AddConstMap G G a a) | {G : Type u_1} → [inst : Add G] → {a : G} → One (AddConstMap G G a a) | [
[
"AddConstMap"
],
[
"Add"
],
[
"One"
]
] | [
[
"\"AddConstMap\""
],
[
"\"One\"",
"\"mk\""
],
[
"\"AddConstMap\"",
"\"id\""
]
] |
false | definition | [
"\"AddConstMap\"",
"\"casesOn\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} {motive : (AddConstMap.{u_1, u_2} G H [email protected]._hyg... | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} →
{b : H} →
{motive : AddConstMap G H a b → Sort u} →
(t : AddConstMap G H a b) →
((toFun : G → H) →
(map_add_const' : ∀ (x : G), toFun (x + a) = toFu... | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} →
{b : H} →
{motive : AddConstMap G H a b → Sort u} →
(t : AddConstMap G H a b) →
((toFun : G → H) →
(map_add_const' : ∀ (x : G), toFun (x + a) = toFu... | [
[
"HAdd",
"hAdd"
],
[
"AddConstMap",
"mk"
],
[
"AddConstMap"
],
[
"instHAdd"
],
[
"Add"
],
[
"Eq"
]
] | [
[
"\"AddConstMap\"",
"\"rec\""
]
] |
true | theorem | [
"\"AddConstMapClass\"",
"\"monotone_iff_Icc\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {a : G} {b : H} [[email protected]._hygCtx._hyg.12 : AddCommGroup.{u_2} G] [[email protected].... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
[inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
[IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
0 < a → ∀ (l : G), Monoto... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
[inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
[IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
0 < a → ∀ (l : G), Monoto... | [
[
"SubtractionMonoid",
"toSubNegZeroMonoid"
],
[
"PartialOrder",
"toPreorder"
],
[
"Set",
"Icc"
],
[
"Preorder",
"toLT"
],
[
"SubtractionCommMonoid",
"toSubtractionMonoid"
],
[
"DFunLike",
"coe"
],
[
"SubNegZeroMonoid",
"toNegZeroClass"... | [
[
"\"PartialOrder\"",
"\"toPreorder\""
],
[
"\"Set\"",
"\"Icc\""
],
[
"\"AddCommGroup\"",
"\"toAddGroup\""
],
[
"\"Preorder\"",
"\"toLT\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"Iff\"",
"\"intro\""
],
[
"\"instDistribLatticeOfLinearOrder\""... |
true | theorem | [
"\"AddConstMap\"",
"\"coe_vadd\"",
"\"_simp_1\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} {K : Type.{u_3}} [[email protected]._hygCtx._hyg.13 : VAdd.{u_3, u... | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {K : Type u_3} [inst_2 : VAdd K H]
[inst_3 : VAddAssocClass K H H] (c : K) (f : AddConstMap G H a b), c +ᵥ ⇑f = ⇑(c +ᵥ f) | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {K : Type u_3} [inst_2 : VAdd K H]
[inst_3 : VAddAssocClass K H H] (c : K) (f : AddConstMap G H a b), c +ᵥ ⇑f = ⇑(c +ᵥ f) | [
[
"VAdd"
],
[
"instHVAdd"
],
[
"AddConstMap"
],
[
"Add"
],
[
"Add",
"toVAdd"
],
[
"AddConstMap",
"instVAddOfVAddAssocClass"
],
[
"Function",
"hasVAdd"
],
[
"Eq"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
... | [
[
"\"instHVAdd\""
],
[
"\"AddConstMap\""
],
[
"\"Eq\"",
"\"symm\""
],
[
"\"AddConstMap\"",
"\"coe_vadd\""
],
[
"\"Function\"",
"\"hasVAdd\""
],
[
"\"AddConstMap\"",
"\"instVAddOfVAddAssocClass\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"H... |
true | theorem | [
"\"AddConstMap\"",
"\"toEnd\"",
"\"_proof_2\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G} ([email protected]._hygCtx._hyg.37 : AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]... | ∀ {G : Type u_1} [inst : Add G] {a : G} (x x_1 : AddConstMap G G a a), ⇑(x * x_1) = ⇑(x * x_1) | ∀ {G : Type u_1} [inst : Add G] {a : G} (x x_1 : AddConstMap G G a a), ⇑(x * x_1) = ⇑(x * x_1) | [
[
"MulOneClass",
"toMulOne"
],
[
"MulOne",
"toMul"
],
[
"AddConstMap",
"instMonoid"
],
[
"AddConstMap"
],
[
"Add"
],
[
"Monoid",
"toMulOneClass"
],
[
"instHMul"
],
[
"HMul",
"hMul"
],
[
"Function",
"End"
],
[
"Eq"
... | [
[
"\"MulOneClass\"",
"\"toMulOne\""
],
[
"\"rfl\""
],
[
"\"MulOne\"",
"\"toMul\""
],
[
"\"AddConstMap\"",
"\"instMonoid\""
],
[
"\"AddConstMap\""
],
[
"\"Monoid\"",
"\"toMulOneClass\""
],
[
"\"instHMul\""
],
[
"\"HMul\"",
"\"hMul\""
]... |
false | definition | [
"\"AddConstMap\"",
"\"replaceConsts\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H}, (AddConstMap.{u_1, u_2} G H [email protected]._hygCtx._hyg.... | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} → {b : H} → AddConstMap G H a b → (a' : G) → (b' : H) → a = a' → b = b' → AddConstMap G H a' b' | {G : Type u_1} →
{H : Type u_2} →
[inst : Add G] →
[inst_1 : Add H] →
{a : G} → {b : H} → AddConstMap G H a b → (a' : G) → (b' : H) → a = a' → b = b' → AddConstMap G H a' b' | [
[
"AddConstMap"
],
[
"Add"
],
[
"Eq"
]
] | [
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"AddConstMap\"",
"\"replaceConsts\"",
"\"_proof_1\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"addLeftHom\"",
"\"_proof_2\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.3 : AddMonoid.{u_1} G] {a : G} ([email protected]._hygCtx._hyg.42 : Multiplicative.{u_1} G) ([email protected]._hygCtx._hyg.44 : Multiplicative.{u_1} G), Eq.{succ u_... | ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} (x x_1 : Multiplicative G),
Multiplicative.toAdd (x * x_1) +ᵥ AddConstMap.id =
(Multiplicative.toAdd x +ᵥ AddConstMap.id) * (Multiplicative.toAdd x_1 +ᵥ AddConstMap.id) | ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} (x x_1 : Multiplicative G),
Multiplicative.toAdd (x * x_1) +ᵥ AddConstMap.id =
(Multiplicative.toAdd x +ᵥ AddConstMap.id) * (Multiplicative.toAdd x_1 +ᵥ AddConstMap.id) | [
[
"MulOneClass",
"toMulOne"
],
[
"Multiplicative",
"toAdd"
],
[
"Equiv",
"instEquivLike"
],
[
"HMul",
"hMul"
],
[
"DFunLike",
"coe"
],
[
"Equiv"
],
[
"AddConstMap",
"id"
],
[
"AddAction",
"toAddSemigroupAction"
],
[
"Mul... | [
[
"\"MulOneClass\"",
"\"toMulOne\""
],
[
"\"Multiplicative\"",
"\"toAdd\""
],
[
"\"Equiv\"",
"\"instEquivLike\""
],
[
"\"HMul\"",
"\"hMul\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
],
[
"\"Equiv\""
],
[
... |
true | theorem | [
"\"_private\"",
"\"Mathlib\"",
"\"Algebra\"",
"\"AddConstMap\"",
"\"Basic\"",
"0",
"\"AddConstMapClass\"",
"\"map_add_nat'\"",
"\"_simp_1_1\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {a : G} {b : H} [[email protected]._hygCtx._hyg.12 : AddMonoid.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddMonoid G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f x + n • b = f (x + n • a) | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddMonoid G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f x + n • b = f (x + n • a) | [
[
"FunLike"
],
[
"instHAdd"
],
[
"AddMonoid"
],
[
"AddConstMapClass"
],
[
"DFunLike",
"coe"
],
[
"HAdd",
"hAdd"
],
[
"Nat"
],
[
"AddMonoid",
"toNSMul"
],
[
"AddMonoid",
"toAddSemigroup"
],
[
"HSMul",
"hSMul"
],
[
... | [
[
"\"HAdd\"",
"\"hAdd\""
],
[
"\"Nat\""
],
[
"\"AddMonoid\"",
"\"toNSMul\""
],
[
"\"instHAdd\""
],
[
"\"AddMonoid\"",
"\"toAddSemigroup\""
],
[
"\"AddConstMapClass\"",
"\"map_add_nsmul\""
],
[
"\"HSMul\"",
"\"hSMul\""
],
[
"\"Eq\"",
... |
false | definition | [
"\"AddConstMap\"",
"\"_aux_Mathlib_Algebra_AddConstMap_Basic___unexpand_AddConstMap_1\""
] | Lean.PrettyPrinter.Unexpander | Lean.PrettyPrinter.Unexpander | Lean.PrettyPrinter.Unexpander | [
[
"Lean",
"PrettyPrinter",
"Unexpander"
]
] | [
[
"\"Lean\"",
"\"Name\""
],
[
"\"Lean\"",
"\"TSyntax\"",
"\"raw\""
],
[
"\"Bool\"",
"false"
],
[
"\"Lean\"",
"\"MonadQuotation\"",
"\"getCurrMacroScope\""
],
[
"\"Lean\"",
"\"MacroScope\""
],
[
"\"Lean\"",
"\"SourceInfo\""
],
[
"\"L... |
true | theorem | [
"\"AddConstMap\"",
"\"mkFract\"",
"\"_proof_4\""
] | forall {R : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Ring.{u_1} R] [[email protected]._hygCtx._hyg.7 : LinearOrder.{u_1} R] [[email protected]._hygCtx._hyg.10 : IsStrictOrderedRing.{u_1} R (Ring.toSemiring.{u... | ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (x : R),
0 ≤ Int.fract x ∧ Int.fract x < 1 | ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (x : R),
0 ≤ Int.fract x ∧ Int.fract x < 1 | [
[
"PartialOrder",
"toPreorder"
],
[
"Ring",
"toNonAssocRing"
],
[
"Preorder",
"toLT"
],
[
"AddGroupWithOne",
"toAddMonoidWithOne"
],
[
"instDistribLatticeOfLinearOrder"
],
[
"NonUnitalNonAssocRing",
"toNonUnitalNonAssocSemiring"
],
[
"Ring",
... | [
[
"\"Int\"",
"\"fract_nonneg\""
],
[
"\"Ring\"",
"\"toNonAssocRing\""
],
[
"\"PartialOrder\"",
"\"toPreorder\""
],
[
"\"Lattice\"",
"\"toSemilatticeInf\""
],
[
"\"Preorder\"",
"\"toLT\""
],
[
"\"AddGroupWithOne\"",
"\"toAddMonoidWithOne\""
],
[... |
true | theorem | [
"\"AddConstMap\"",
"\"mk\"",
"\"congr_simp\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} (toFun : G -> H) (toFun_1 : G -> H) (e_toFun : Eq.{max (succ u_1) (succ u_2)} (G -> H) toFun to... | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (toFun toFun_1 : G → H)
(e_toFun : toFun = toFun_1) (map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b),
{ toFun := toFun, map_add_const' := map_add_const' } = { toFun := toFun_1, map_add_const' := ⋯ } | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (toFun toFun_1 : G → H)
(e_toFun : toFun = toFun_1) (map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b),
{ toFun := toFun, map_add_const' := map_add_const' } = { toFun := toFun_1, map_add_const' := ⋯ } | [
[
"HAdd",
"hAdd"
],
[
"AddConstMap",
"mk"
],
[
"AddConstMap"
],
[
"instHAdd"
],
[
"Add"
],
[
"Eq",
"ndrec"
],
[
"Eq"
]
] | [
[
"\"HAdd\"",
"\"hAdd\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"instHAdd\""
],
[
"\"Eq\"",
"\"refl\""
],
[
"\"Eq\"",
"\"ndrec\""
],
[
"\"Eq\""
],
[
"\"Eq\"",
"\"rec\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"conjNeg\"",
"\"_proof_4\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : AddCommGroup.{u_1} G] [[email protected]._hygCtx._hyg.7 : AddCommGroup.{u_2} H] {a : G} {b : H} ([email protected]._hygCtx._hyg.62 : AddConst... | ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] {a : G} {b : H}
(x : AddConstMap G H a b),
{ toFun := fun x_1 => -{ toFun := fun x_2 => -x (-x_2), map_add_const' := ⋯ } (-x_1), map_add_const' := ⋯ } = x | ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] {a : G} {b : H}
(x : AddConstMap G H a b),
{ toFun := fun x_1 => -{ toFun := fun x_2 => -x (-x_2), map_add_const' := ⋯ } (-x_1), map_add_const' := ⋯ } = x | [
[
"SubtractionMonoid",
"toSubNegZeroMonoid"
],
[
"AddConstMap"
],
[
"AddConstMap",
"mk"
],
[
"Neg",
"neg"
],
[
"AddConstMap",
"conjNeg",
"_proof_1"
],
[
"AddCommGroup"
],
[
"SubtractionCommMonoid",
"toSubtractionMonoid"
],
[
"DFunLi... | [
[
"\"SubtractionMonoid\"",
"\"toSubNegZeroMonoid\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"Neg\"",
"\"neg\""
],
[
"\"AddConstMap\"",
"\"conjNeg\"",
"\"_proof_1\""
],
[
"\"SubtractionCommMonoid\"",
"\"toSubtractionMonoid\""
... |
true | theorem | [
"\"_private\"",
"\"Mathlib\"",
"\"Algebra\"",
"\"AddConstMap\"",
"\"Basic\"",
"0",
"\"AddConstMapClass\"",
"\"rel_map_of_Icc\"",
"\"_proof_1_2\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {a : G} [[email protected]._hygCtx._hyg.12 : AddCommGroup.{u_2} G] [[email protected].... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} [inst_1 : AddCommGroup G]
[inst_2 : LinearOrder G] [IsOrderedAddMonoid G] {f : F} {R : H → H → Prop} {l : G},
(∀ x ∈ Set.Icc l (l + a), ∀ y ∈ Set.Icc l (l + a), x < y → R (f x) (f y)) →
∀ (x y : G), x ∈ Set.Ico l (l + a) → R (f x) (f ... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} [inst_1 : AddCommGroup G]
[inst_2 : LinearOrder G] [IsOrderedAddMonoid G] {f : F} {R : H → H → Prop} {l : G},
(∀ x ∈ Set.Icc l (l + a), ∀ y ∈ Set.Icc l (l + a), x < y → R (f x) (f y)) →
∀ (x y : G), x ∈ Set.Ico l (l + a) → R (f x) (f ... | [
[
"PartialOrder",
"toPreorder"
],
[
"Set",
"Icc"
],
[
"AddCommGroup",
"toAddGroup"
],
[
"Membership",
"mem"
],
[
"Preorder",
"toLT"
],
[
"DFunLike",
"coe"
],
[
"instDistribLatticeOfLinearOrder"
],
[
"IsOrderedAddMonoid"
],
[
... | [
[
"\"SubtractionMonoid\"",
"\"toSubNegZeroMonoid\""
],
[
"\"PartialOrder\"",
"\"toPreorder\""
],
[
"\"Eq\"",
"\"trans\""
],
[
"\"Lean\"",
"\"Grind\"",
"\"Order\"",
"\"le_eq_true_of_lt\""
],
[
"\"AddCommGroup\"",
"\"toAddGroup\""
],
[
"\"Members... |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_ofNat'\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] {b : H} [[email protected]._hygCtx._hyg.12 : AddMonoidWithOne.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo],
f (OfNat.ofNat n) = f 0 + OfNat.ofNat n • b | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
[inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo],
f (OfNat.ofNat n) = f 0 + OfNat.ofNat n • b | [
[
"AddMonoidWithOne",
"toAddMonoid"
],
[
"DFunLike",
"coe"
],
[
"instOfNatNat"
],
[
"Nat",
"AtLeastTwo"
],
[
"instHSMul"
],
[
"Zero",
"toOfNat0"
],
[
"Eq"
],
[
"AddMonoidWithOne"
],
[
"AddSemigroup",
"toAdd"
],
[
"FunLik... | [
[
"\"AddConstMapClass\"",
"\"map_nat'\""
]
] |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_ofNat_add\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] [[email protected]._hygCtx._hyg.12 : AddCommMonoidWithOne.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddCommMonoidWithOne G]
[inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo] (x : G),
f (OfNat.ofNat n + x) = f x + OfNat.ofNat n | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddCommMonoidWithOne G]
[inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo] (x : G),
f (OfNat.ofNat n + x) = f x + OfNat.ofNat n | [
[
"FunLike"
],
[
"instHAdd"
],
[
"instOfNatAtLeastTwo"
],
[
"AddConstMapClass"
],
[
"AddMonoidWithOne",
"toAddMonoid"
],
[
"DFunLike",
"coe"
],
[
"OfNat",
"ofNat"
],
[
"HAdd",
"hAdd"
],
[
"Nat"
],
[
"AddMonoidWithOne",
"... | [
[
"\"AddConstMapClass\"",
"\"map_nat_add\""
]
] |
false | definition | [
"\"AddConstMap\"",
"\"instPowNat\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, Pow.{u_1, 0} (AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) Nat | {G : Type u_1} → [inst : Add G] → {a : G} → Pow (AddConstMap G G a a) ℕ | {G : Type u_1} → [inst : Add G] → {a : G} → Pow (AddConstMap G G a a) ℕ | [
[
"Nat"
],
[
"AddConstMap"
],
[
"Add"
],
[
"Pow"
]
] | [
[
"\"AddConstMap\"",
"\"instPowNat\"",
"\"_proof_1\""
],
[
"\"Nat\""
],
[
"\"Nat\"",
"\"iterate\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
],
[
... |
true | theorem | [
"\"AddConstMap\"",
"\"toFun_eq_coe\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} (f : AddConstMap.{u_1, u_2} G H [email protected]._hygCtx._h... | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b), f.toFun = ⇑f | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b), f.toFun = ⇑f | [
[
"AddConstMap"
],
[
"Add"
],
[
"AddConstMap",
"toFun"
],
[
"Eq"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
]
] | [
[
"\"rfl\""
],
[
"\"AddConstMap\"",
"\"toFun\""
]
] |
false | definition | [
"\"AddConstMap\"",
"\"instInhabited\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] {a : G}, Inhabited.{succ u_1} (AddConstMap.{u_1, u_1} G G [email protected]._hygCtx._hyg.4 [email protected]._hygCtx._hyg.4 a a) | {G : Type u_1} → [inst : Add G] → {a : G} → Inhabited (AddConstMap G G a a) | {G : Type u_1} → [inst : Add G] → {a : G} → Inhabited (AddConstMap G G a a) | [
[
"AddConstMap"
],
[
"Add"
],
[
"Inhabited"
]
] | [
[
"\"Inhabited\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"id\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"conjNeg\"",
"\"_proof_2\""
] | forall {G : Type.{u_2}} {H : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : AddCommGroup.{u_2} G] [[email protected]._hygCtx._hyg.7 : AddCommGroup.{u_1} H] {a : G} {b : H} ([email protected]._hygCtx._hyg.62 : AddConst... | ∀ {G : Type u_2} {H : Type u_1} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] {a : G} {b : H}
(x : AddConstMap G H a b) (x_1 : G),
-{ toFun := fun x_2 => -x (-x_2), map_add_const' := ⋯ } (-(x_1 + a)) =
-{ toFun := fun x_2 => -x (-x_2), map_add_const' := ⋯ } (-x_1) + b | ∀ {G : Type u_2} {H : Type u_1} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] {a : G} {b : H}
(x : AddConstMap G H a b) (x_1 : G),
-{ toFun := fun x_2 => -x (-x_2), map_add_const' := ⋯ } (-(x_1 + a)) =
-{ toFun := fun x_2 => -x (-x_2), map_add_const' := ⋯ } (-x_1) + b | [
[
"SubtractionMonoid",
"toSubNegZeroMonoid"
],
[
"AddConstMap",
"mk"
],
[
"AddConstMap"
],
[
"instHAdd"
],
[
"Neg",
"neg"
],
[
"AddConstMap",
"conjNeg",
"_proof_1"
],
[
"AddCommGroup"
],
[
"SubtractionCommMonoid",
"toSubtractionMono... | [
[
"\"SubtractionMonoid\"",
"\"toSubNegZeroMonoid\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"Neg\"",
"\"neg\""
],
[
"\"AddConstMap\"",
"\"conjNeg\"",
"\"_proof_1\""
],
[
"\"SubtractionCommMonoid\"",
"\"toSubtractionMonoid\""
... |
true | theorem | [
"\"_private\"",
"\"Mathlib\"",
"\"Algebra\"",
"\"AddConstMap\"",
"\"Basic\"",
"0",
"\"AddConstMapClass\"",
"\"rel_map_of_Icc\"",
"\"_simp_1_3\""
] | forall {G : Type.{u_1}} [[email protected]._hygCtx._hyg.3 : AddSemigroup.{u_1} G] (a : G) (b : G) (c : G), Eq.{succ u_1} G (HAdd.hAdd.{u_1, u_1, u_1} G G G (instHAdd.{u_1} G (AddSemigroup.toAdd.{u_1} G [email protected]._hygCtx._hyg.3)) a (HAdd.hAdd.{u_1, u_1, u_1... | ∀ {G : Type u_1} [inst : AddSemigroup G] (a b c : G), a + (b + c) = a + b + c | ∀ {G : Type u_1} [inst : AddSemigroup G] (a b c : G), a + (b + c) = a + b + c | [
[
"HAdd",
"hAdd"
],
[
"AddSemigroup"
],
[
"instHAdd"
],
[
"Eq"
],
[
"AddSemigroup",
"toAdd"
]
] | [
[
"\"HAdd\"",
"\"hAdd\""
],
[
"\"instHAdd\""
],
[
"\"add_assoc\""
],
[
"\"Eq\"",
"\"symm\""
],
[
"\"AddSemigroup\"",
"\"toAdd\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"mkFract\"",
"\"_proof_1\""
] | forall {R : Type.{u_2}} {G : Type.{u_1}} [[email protected]._hygCtx._hyg.4 : Ring.{u_2} R] [[email protected]._hygCtx._hyg.7 : LinearOrder.{u_2} R] [[email protected]._hygCtx._hyg.10 : IsStrictOrderedRing.{u_2} R (R... | ∀ {R : Type u_2} {G : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R]
[inst_3 : FloorRing R] [inst_4 : AddGroup G] (a : G) (f : ↑(Set.Ico 0 1) → G) (x : R),
(fun x => f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a) (x + 1) = (fun x => f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a) x + a | ∀ {R : Type u_2} {G : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R]
[inst_3 : FloorRing R] [inst_4 : AddGroup G] (a : G) (f : ↑(Set.Ico 0 1) → G) (x : R),
(fun x => f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a) (x + 1) = (fun x => f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a) x + a | [
[
"Ring",
"toNonAssocRing"
],
[
"PartialOrder",
"toPreorder"
],
[
"Membership",
"mem"
],
[
"Preorder",
"toLT"
],
[
"AddGroupWithOne",
"toAddMonoidWithOne"
],
[
"Set",
"Elem"
],
[
"NonUnitalNonAssocRing",
"toNonUnitalNonAssocSemiring"
... | [
[
"\"Ring\"",
"\"toNonAssocRing\""
],
[
"\"PartialOrder\"",
"\"toPreorder\""
],
[
"\"Eq\"",
"\"trans\""
],
[
"\"Membership\"",
"\"mem\""
],
[
"\"Preorder\"",
"\"toLT\""
],
[
"\"Int\"",
"\"floor_add_one\""
],
[
"\"Subtype\"",
"\"mk\"",
... |
true | theorem | [
"\"AddConstMap\"",
"\"mk_coe\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} (f : AddConstMap.{u_1, u_2} G H [email protected]._hygCtx._h... | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b),
{ toFun := ⇑f, map_add_const' := ⋯ } = f | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b),
{ toFun := ⇑f, map_add_const' := ⋯ } = f | [
[
"AddConstMap",
"mk"
],
[
"AddConstMap"
],
[
"Add"
],
[
"AddConstMap",
"map_add_const'"
],
[
"Eq"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
]
] | [
[
"\"rfl\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"AddConstMap\"",
"\"map_add_const'\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
]
] |
true | theorem | [
"\"AddConstMap\"",
"\"coe_mk\""
] | forall {G : Type.{u_1}} {H : Type.{u_2}} [[email protected]._hygCtx._hyg.4 : Add.{u_1} G] [[email protected]._hygCtx._hyg.7 : Add.{u_2} H] {a : G} {b : H} (f : G -> H) (hf : forall (x : G), Eq.{succ u_2} H (f (HAdd.hAdd.{u_1, u_1, u_1} G G G (instHAd... | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : G → H)
(hf : ∀ (x : G), f (x + a) = f x + b), ⇑{ toFun := f, map_add_const' := hf } = f | ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : G → H)
(hf : ∀ (x : G), f (x + a) = f x + b), ⇑{ toFun := f, map_add_const' := hf } = f | [
[
"HAdd",
"hAdd"
],
[
"AddConstMap",
"mk"
],
[
"AddConstMap"
],
[
"instHAdd"
],
[
"Add"
],
[
"Eq"
],
[
"DFunLike",
"coe"
],
[
"AddConstMap",
"instFunLike"
]
] | [
[
"\"rfl\""
],
[
"\"AddConstMap\"",
"\"mk\""
],
[
"\"AddConstMap\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMap\"",
"\"instFunLike\""
]
] |
true | theorem | [
"\"AddConstMapClass\"",
"\"map_nat\""
] | forall {F : Type.{u_1}} {G : Type.{u_2}} {H : Type.{u_3}} [[email protected]._hygCtx._hyg.5 : FunLike.{succ u_1, succ u_2, succ u_3} F G H] [[email protected]._hygCtx._hyg.12 : AddMonoidWithOne.{u_2} G] [[email protected]... | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddMonoidWithOne G]
[inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ), f ↑n = f 0 + ↑n | ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddMonoidWithOne G]
[inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ), f ↑n = f 0 + ↑n | [
[
"FunLike"
],
[
"Nat",
"cast"
],
[
"instHAdd"
],
[
"AddConstMapClass"
],
[
"AddZeroClass",
"toAddZero"
],
[
"AddMonoidWithOne",
"toAddMonoid"
],
[
"DFunLike",
"coe"
],
[
"OfNat",
"ofNat"
],
[
"HAdd",
"hAdd"
],
[
"Na... | [
[
"\"Nat\"",
"\"cast\""
],
[
"\"Eq\"",
"\"trans\""
],
[
"\"AddMonoidWithOne\"",
"\"toAddMonoid\""
],
[
"\"DFunLike\"",
"\"coe\""
],
[
"\"AddConstMapClass\"",
"\"map_nat'\""
],
[
"\"congrArg\""
],
[
"\"instHSMul\""
],
[
"\"Zero\"",
"... |
End of preview.
YAML Metadata Warning:empty or missing yaml metadata in repo card
Check out the documentation for more information.
MATHLIB4 DEPENDENCY GRAPH
make dependency graph for mathlib4 using jixia
HOW TO
how to make your own mathlib4 graph
Clone the repository at https://github.com/fbundle/mathlib4_dependency_graph
Check out your favorite mathlib version
Use
buildscript to build mathlib and jixiaExtract dependency graph by
jixia_export.pyGet symbol file by
get_symbol_file.pyandget_symbol_db.pyUpload to huggingface using
upload_huggingface.py
or just download the prebuilt files using download_huggingface.py
PREBUILT GRAPH
- Downloads last month
- 19