Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/gist:581494327bb58f5d84bc17882304460a

Created November 23, 2020 22:21
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kbuzzard/581494327bb58f5d84bc17882304460a to your computer and use it in GitHub Desktop.
Save kbuzzard/581494327bb58f5d84bc17882304460a to your computer and use it in GitHub Desktop.
Download ZIP
goal
Raw
gistfile1.txt
⊢ @eq.{1} nat
(@fintype.card.{u_2}
(@alg_equiv.{u_1 u_2 u_2} F
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@comm_ring.to_comm_semiring.{u_1} F
(@euclidean_domain.to_comm_ring.{u_1} F (@field.to_euclidean_domain.{u_1} F _inst_1)))
(@ring.to_semiring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@division_ring.to_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@field.to_division_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@intermediate_field.to_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α))))))
(@ring.to_semiring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@division_ring.to_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@field.to_division_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@intermediate_field.to_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α))))))
(@intermediate_field.algebra.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@intermediate_field.algebra.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α))))
(@alg_equiv.fintype.{u_1 u_2} F
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
_inst_1
(@intermediate_field.to_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@intermediate_field.algebra.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@intermediate_field.finite_dimensional_left.{u_1 u_2} F E _inst_1 _inst_2 _inst_3 _inst_4
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))))
(@finite_dimensional.findim.{u_2 u_1} F
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
_inst_1
(@ring.to_add_comm_group.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@division_ring.to_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@field.to_division_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@intermediate_field.to_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α))))))
(@algebra.to_semimodule.{u_1 u_2} F
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@comm_ring.to_comm_semiring.{u_1} F
(@euclidean_domain.to_comm_ring.{u_1} F (@field.to_euclidean_domain.{u_1} F _inst_1)))
(@ring.to_semiring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@division_ring.to_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@field.to_division_ring.{u_2}
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
(@intermediate_field.to_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α))))))
(@intermediate_field.algebra.{u_1 u_2} F E _inst_1 _inst_2 _inst_3
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment