Jz Pan
Jz Pan
also move `lTensor_inj_iff_rTensor_inj` to `LinearMap` --- [](https://gitpod.io/from-referrer/)
--- - [ ] depends on: #12434 [part one: submodule version] - [x] depends on: #11635 - [x] depends on: #11598 [need `finsuppTensorFinsupp'_symm_single`] - [x] depends on: #11731 - [x]...
- `TensorProduct.congr_symm` which states `(TensorProduct.congr f g).symm = TensorProduct.congr f.symm g.symm` - `TensorProduct.coe_congr_(left|right)_refl`: relates `TensorProduct.congr` and `LinearMap.(l|r)Tensor` --- [](https://gitpod.io/from-referrer/)
Try this level: ~~~ size=800,600 tile(PlayerStart,0,0,50,50) tile(ShadowStart,0,50,50,50) tile(ConveyorBelt,0,250,350,50){ activated=1 speed=10 } tile(Block,350,200,100,100) tile(MovingBlock,49,225,50,50){ MovingPosCount=2 activated=1 id=1 loop=1 t0=2500 t1=2500 x0=250 x1=0 y0=0 y1=0 } ~~~ You will find that the...
... which state that if - `R` is a ring (not necessarily commutative) and `M` is a Noetherian `R`-module (based on the proof in ), or - `R` is a...
... from requiring `F` being a field to `F` satisfying `StrongRankCondition` and `S` being a free `F`-module. This makes the original statement a special case. The changed results are: `Subalgebra.eq_bot_of_(rank_le|finrank)_one`,...
We use `md4c` to process markdown with LaTeX formulas which is fed to MathJax, which prefers `$` or `\(` directly. I have a working implementation which added two options `MD_HTML_FLAG_MATHJAX`...
Currently the XHTML render of the following markdown ```markdown - [ ] Is this valid XHTML? - [x] Is this valid XHTML? ``` is ```html Is this valid XHTML? Is...
This PR adds two options `MD_HTML_FLAG_MATHJAX` and `MD_HTML_FLAG_MATHJAX_USE_DOLLAR`: - if `MD_HTML_FLAG_MATHJAX` is enabled, it will output `\(`, `\)`, `\[`, `\]` instead of `` in html output; - if both of...
This addresses first two points of issue #281. - Since `OFF_MAX` is not used in the code at all, I just remove it. - `SZ_MAX` is used only at one...