Skip to content

Instantly share code, notes, and snippets.

@kbuzzard
Created May 24, 2021 08:59
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/799ace8f2b25e45da5b03aad5c92f554 to your computer and use it in GitHub Desktop.
Save kbuzzard/799ace8f2b25e45da5b03aad5c92f554 to your computer and use it in GitHub Desktop.
@is_scalar_tower ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smul_with_zero.to_has_scalar ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@mul_zero_class.to_has_zero ๐•œ
(@mul_zero_one_class.to_mul_zero_class ๐•œ
(@monoid_with_zero.to_mul_zero_one_class ๐•œ
(@semiring.to_monoid_with_zero ๐•œ
(@comm_semiring.to_semiring ๐•œ
(@comm_ring.to_comm_semiring ๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))))
(@add_zero_class.to_has_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_monoid.to_add_zero_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_monoid.to_add_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@semiring.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_)))))))
(@mul_action_with_zero.to_smul_with_zero ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@semiring.to_monoid_with_zero ๐•œ
(@comm_semiring.to_semiring ๐•œ
(@comm_ring.to_comm_semiring ๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@add_zero_class.to_has_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_monoid.to_add_zero_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_monoid.to_add_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@semiring.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_)))))))
(@module.to_mul_action_with_zero ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring ๐•œ
(@comm_ring.to_comm_semiring ๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@semiring.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_))))
(@algebra.to_module ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring ๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))
(@comm_semiring.to_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_)))
(@times_cont_mdiff_map.algebra ๐•œ _inst_1 E _inst_2 _inst_3 H _inst_4 I M _inst_5 _inst_6 ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))
(@normed_algebra.id ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
_)))))
(@smul_with_zero.to_has_scalar C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@mul_zero_class.to_has_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@mul_zero_one_class.to_mul_zero_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@monoid_with_zero.to_mul_zero_one_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@semiring.to_monoid_with_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_)))))))
(@add_zero_class.to_has_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_monoid.to_add_zero_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_monoid.to_add_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_cancel_comm_monoid.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_group.to_cancel_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_add_comm_group ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@lie_ring.to_add_comm_group ๐•œ
(@lie_ring.of_associative_ring ๐•œ
(@normed_ring.to_ring ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_))))))
(@mul_action_with_zero.to_smul_with_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@semiring.to_monoid_with_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_))))
(@add_zero_class.to_has_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_monoid.to_add_zero_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_monoid.to_add_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_cancel_comm_monoid.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_group.to_cancel_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_add_comm_group ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@lie_ring.to_add_comm_group ๐•œ
(@lie_ring.of_associative_ring ๐•œ
(@normed_ring.to_ring ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_))))))
(@module.to_mul_action_with_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_ring.to_comm_semiring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_)))
(@add_cancel_comm_monoid.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_group.to_cancel_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_add_comm_group ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@lie_ring.to_add_comm_group ๐•œ
(@lie_ring.of_associative_ring ๐•œ
(@normed_ring.to_ring ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_)))
(@smooth_map_module' ๐•œ _inst_1 E _inst_2 _inst_3 H _inst_4 I M _inst_5 _inst_6 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@smul_with_zero.to_has_scalar ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@mul_zero_class.to_has_zero ๐•œ
(@mul_zero_one_class.to_mul_zero_class ๐•œ
(@monoid_with_zero.to_mul_zero_one_class ๐•œ
(@semiring.to_monoid_with_zero ๐•œ
(@comm_semiring.to_semiring ๐•œ
(@comm_ring.to_comm_semiring ๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))))
(@add_zero_class.to_has_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_monoid.to_add_zero_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_monoid.to_add_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_cancel_comm_monoid.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_group.to_cancel_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_add_comm_group ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@lie_ring.to_add_comm_group ๐•œ
(@lie_ring.of_associative_ring ๐•œ
(@normed_ring.to_ring ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_))))))
(@mul_action_with_zero.to_smul_with_zero ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@semiring.to_monoid_with_zero ๐•œ
(@comm_semiring.to_semiring ๐•œ
(@comm_ring.to_comm_semiring ๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@add_zero_class.to_has_zero C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_monoid.to_add_zero_class C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_monoid.to_add_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_cancel_comm_monoid.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_group.to_cancel_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_add_comm_group ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@lie_ring.to_add_comm_group ๐•œ
(@lie_ring.of_associative_ring ๐•œ
(@normed_ring.to_ring ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_))))))
(@module.to_mul_action_with_zero ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@comm_semiring.to_semiring ๐•œ
(@comm_ring.to_comm_semiring ๐•œ
(@semi_normed_comm_ring.to_comm_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@add_cancel_comm_monoid.to_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@add_comm_group.to_cancel_add_comm_monoid C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
(@smooth_map_add_comm_group ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
H
_inst_4
I
๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
๐“˜(๐•œ, ๐•œ)
M
_inst_5
_inst_6
๐•œ
(@lie_ring.to_add_comm_group ๐•œ
(@lie_ring.of_associative_ring ๐•œ
(@normed_ring.to_ring ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_ring.to_pseudo_metric_space ๐•œ
(@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
(@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
(@charted_space_self ๐•œ
(@uniform_space.to_topological_space ๐•œ
(@metric_space.to_uniform_space' ๐•œ
(@semi_normed_group.to_pseudo_metric_space ๐•œ
(@normed_group.to_semi_normed_group ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ
(@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
_)))
(@smooth_map_module ๐•œ _inst_1 E _inst_2 _inst_3 H _inst_4 I M _inst_5 _inst_6 ๐•œ
(@normed_ring.to_normed_group ๐•œ
(@normed_comm_ring.to_normed_ring ๐•œ
(@normed_field.to_normed_comm_ring ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
(@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment