GLnDefs

📁 Source: FLT/GlobalLanglandsConjectures/GLnDefs.lean

Statistics

Metric	Count
Definitions `Alg`, `AutomorphicFormForGLnOverQ`, `instCoeFunForallProdGeneralLinearGroupFinFiniteAdeleRingIntRatRealComplex`, `toFun`, `IsConstantOn`, `IsSlowlyIncreasing`, `IsSmooth`, `baseChange`, `baseChange`, `Weight`, `w`, `Z`, `action`, `actionTensorC`, `actionTensorCAlg`, `actionTensorCAlg'`, `actionTensorCAlg'2`, `actionTensorCAlg'3`, `annihilator`, `instAddCommMonoidSubtypeAlgMemSubalgebraComplexZ`, `instAlgebraComplexAlg`, `instCommSemiringSubtypeAlgMemSubalgebraComplexZ`, `instModuleComplexContMDiffMapRealModelWithCornersSelfSomeENatTop_fLT`, `instModuleRealContMDiffMapModelWithCornersSelfSomeENatTop_fLT`, `instSemiringAlg`, `preweight`, `d`, `fdRep`, `rho`, `s`, `bracketBilin`, `instLieAlgebra'`, `GL`	33
Theorems `has_finite_level`, `is_finite_cod`, `is_periodic`, `is_slowly_increasing`, `is_smooth`, `finite_level`, `is_compact`, `is_open`, `bounded_by`, `continuous`, `loc_cst`, `smooth`, `isSimple`, `rho_continuous`, `ext`, `ext_iff`, `bracketBilin_apply_apply`, `diamond_fix`	18
Total	51
⚠️ With sorry `actionTensorCAlg'3`, `instModuleComplexContMDiffMapRealModelWithCornersSelfSomeENatTop_fLT`	2

AutomorphicForm.GLn

Definitions

Name	Category	Theorems
`Alg` 📖	CompOp	1 math math: `AutomorphicFormForGLnOverQ.is_finite_cod`
`AutomorphicFormForGLnOverQ` 📖	CompData	—
`IsConstantOn` 📖	CompData	1 math math: `AutomorphicFormForGLnOverQ.has_finite_level`
`IsSlowlyIncreasing` 📖	CompData	1 math math: `AutomorphicFormForGLnOverQ.is_slowly_increasing`
`IsSmooth` 📖	CompData	1 math math: `AutomorphicFormForGLnOverQ.is_smooth`
`Weight` 📖	CompData	—
`Z` 📖	CompOp	1 math math: `AutomorphicFormForGLnOverQ.is_finite_cod`
`action` 📖	CompOp	—
`actionTensorC` 📖	CompOp	—
`actionTensorCAlg` 📖	CompOp	—
`actionTensorCAlg'` 📖	CompOp	—
`actionTensorCAlg'2` 📖	CompOp	—
`actionTensorCAlg'3` 📖 ⚠️	CompOp	1 math math: `AutomorphicFormForGLnOverQ.is_finite_cod`
`annihilator` 📖	CompOp	1 math math: `AutomorphicFormForGLnOverQ.is_finite_cod`
`instAddCommMonoidSubtypeAlgMemSubalgebraComplexZ` 📖	CompOp	—
`instAlgebraComplexAlg` 📖	CompOp	1 math math: `AutomorphicFormForGLnOverQ.is_finite_cod`
`instCommSemiringSubtypeAlgMemSubalgebraComplexZ` 📖	CompOp	—
`instModuleComplexContMDiffMapRealModelWithCornersSelfSomeENatTop_fLT` 📖 ⚠️	CompOp	1 math math: `AutomorphicFormForGLnOverQ.is_finite_cod`
`instModuleRealContMDiffMapModelWithCornersSelfSomeENatTop_fLT` 📖	CompOp	—
`instSemiringAlg` 📖	CompOp	1 math math: `AutomorphicFormForGLnOverQ.is_finite_cod`
`preweight` 📖	CompData	—
`s` 📖	CompOp	1 math math: `IsSlowlyIncreasing.bounded_by`

AutomorphicForm.GLn.AutomorphicFormForGLnOverQ

Definitions

Name	Category	Theorems
`instCoeFunForallProdGeneralLinearGroupFinFiniteAdeleRingIntRatRealComplex` 📖	CompOp	—
`toFun` 📖	CompOp	5 math math: `is_slowly_increasing`, `is_smooth`, `has_finite_level`, `is_finite_cod`, `is_periodic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`has_finite_level` 📖	mathematical	—	`AutomorphicForm.GLn.IsConstantOn` `toFun`	—	—
`is_finite_cod` 📖	mathematical	—	`AutomorphicForm.GLn.Alg` `AutomorphicForm.GLn.instSemiringAlg` `AutomorphicForm.GLn.instAlgebraComplexAlg` `AutomorphicForm.GLn.Z` `IsDedekindDomain.instLieAlgebra'` `AutomorphicForm.GLn.instModuleComplexContMDiffMapRealModelWithCornersSelfSomeENatTop_fLT` `AutomorphicForm.GLn.actionTensorCAlg'3` `AutomorphicForm.GLn.annihilator` `toFun` `AutomorphicForm.GLn.IsSmooth.smooth` `is_smooth`	—	—
`is_periodic` 📖	mathematical	—	`toFun` `RingHom.GL`	—	—
`is_slowly_increasing` 📖	mathematical	—	`AutomorphicForm.GLn.IsSlowlyIncreasing` `toFun`	—	—
`is_smooth` 📖	mathematical	—	`AutomorphicForm.GLn.IsSmooth` `toFun`	—	—

AutomorphicForm.GLn.IsConstantOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_level` 📖	—	`AutomorphicForm.GLn.IsConstantOn`	—	—	—
`is_compact` 📖	—	`AutomorphicForm.GLn.IsConstantOn`	—	—	—
`is_open` 📖	—	`AutomorphicForm.GLn.IsConstantOn`	—	—	—

AutomorphicForm.GLn.IsSlowlyIncreasing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bounded_by` 📖	mathematical	`AutomorphicForm.GLn.IsSlowlyIncreasing`	`AutomorphicForm.GLn.s`	—	—

AutomorphicForm.GLn.IsSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	—	`AutomorphicForm.GLn.IsSmooth`	—	—	—
`loc_cst` 📖	—	`AutomorphicForm.GLn.IsSmooth`	—	—	—
`smooth` 📖	—	`AutomorphicForm.GLn.IsSmooth`	—	—	—

AutomorphicForm.GLn.LieHom

Definitions

Name	Category	Theorems
`baseChange` 📖	CompOp	—

AutomorphicForm.GLn.LieModuleHom

Definitions

Name	Category	Theorems
`baseChange` 📖	CompOp	—

AutomorphicForm.GLn.Weight

Definitions

Name	Category	Theorems
`w` 📖	CompOp	1 math math: `isSimple`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimple` 📖	mathematical	—	`AutomorphicForm.GLn.preweight.fdRep` `w`	—	—

AutomorphicForm.GLn.preweight

Definitions

Name	Category	Theorems
`d` 📖	CompOp	1 math math: `rho_continuous`
`fdRep` 📖	CompOp	1 math math: `AutomorphicForm.GLn.Weight.isSimple`
`rho` 📖	CompOp	1 math math: `rho_continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rho_continuous` 📖	mathematical	—	`d` `rho`	—	—

Bracket

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`

IsDedekindDomain

Definitions

Name	Category	Theorems
`bracketBilin` 📖	CompOp	1 math math: `bracketBilin_apply_apply`
`instLieAlgebra'` 📖	CompOp	1 math math: `AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.is_finite_cod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bracketBilin_apply_apply` 📖	mathematical	—	`bracketBilin`	—	—
`diamond_fix` 📖	—	—	—	—	`Bracket.ext` `bracketBilin_apply_apply`

RingHom

Definitions

Name	Category	Theorems
`GL` 📖	CompOp	1 math math: `AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.is_periodic`

---

← Back to Index