mathlib-dependent-issues-bot comments

Results 94 comments of


                                            mathlib-dependent-issues-bot

feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups

This PR/issue depends on: * ~~leanprover-community/mathlib#15702~~ * ~~leanprover-community/mathlib#15704~~ * ~~leanprover-community/mathlib#15898~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(ring_theory/derivation): Endomorphisms of the Kähler differential module

This PR/issue depends on: * ~~leanprover-community/mathlib#15855~~ * ~~leanprover-community/mathlib#15856~~ * ~~leanprover-community/mathlib#16047~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(algebraic_geometry/morphisms): Construct morphism properties from ring homomorphism properties

This PR/issue depends on: * ~~leanprover-community/mathlib#16060~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(set_theory/cardinal): cardinality of `multiset`, `polynomial` and `mv_polynomial`

This PR/issue depends on: * ~~leanprover-community/mathlib#16046~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(algebra/module/graded_module): define graded module

This PR/issue depends on: * ~~leanprover-community/mathlib#14626~~ * ~~leanprover-community/mathlib#15654~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(algebra/order/floor): The image of `floor`/`ceil` under an order ring hom

This PR/issue depends on: * ~~leanprover-community/mathlib#16024~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

refactor(analysis/normed_space/pi_Lp): make argument of pi_Lp a term of ℝ≥0∞ instead of ℝ

This PR/issue depends on: * ~~leanprover-community/mathlib#15852~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(group_theory/divisible): definition of divisible group

This PR/issue depends on: * ~~leanprover-community/mathlib#15478~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

This PR/issue depends on: * leanprover-community/mathlib#14857 * ~~leanprover-community/mathlib#16052~~ * ~~leanprover-community/mathlib#16054~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!

feat(linear_algebra/clifford_algebra/spin_group) : Spin Group

This PR/issue depends on: * ~~leanprover-community/mathlib#11468~~ * ~~leanprover-community/mathlib#16202~~ * ~~leanprover-community/mathlib#16153~~ By **[Dependent Issues](https://github.com/z0al/dependent-issues)** (🤖). Happy coding!