lean - 精益:定义 R-ideal 和 R-module 的乘积
问题描述
我正在尝试学习精益,我正在尝试弄清楚如何I*M = {i*m | i in I, m in M}
从理想的 I 和 R 模块 M中创建一个新的 R 模块。
所以我的尝试是首先定义一个映射ideal_mult
来创建一个新的 R 模块,然后弄清楚如何为它分配一个好的符号。
import ring_theory.ideals
import algebra.module
universes u v
variables {R : Type u} {M : Type v}
variables [comm_ring R] [add_comm_group M] [module R M]
variables (I: ideal R)
def ideal_mult (I: ideal R) (M: Type v)
[add_comm_group M] [module R M]: Type v
:=
sorry
#check ideal_mult I M
我该如何定义它,以便我可以例如陈述一个假设(h: I*M = M)
?
感谢您的帮助!
解决方案
推荐阅读
- html - Go 模板一起迭代多个数组
- mysql - Mysql docker container - can't get much of anything to work
- python-3.x - 如何将这些添加到字典中并在 python 中每 5 次循环后使一个活动变量结束?
- vuejs2 - 登录后vue路由器导航卫士不重定向
- c# - .NET Core 2.2 - 无法从 Azure AppConfig 获取应用配置
- django - Django 自定义用户模型创建 NOT NULL 约束失败错误
- c - 在 C 中多次使用 Ctrl+C
- python - 从 pdf 中删除打印机裁剪标记
- r - Create a new column based on conditional statement of another column R
- c - 代码只取输入值然后什么都没有发生