ContinuousSMulDiscrete

📁 Source: FLT/Deformations/RepresentationTheory/ContinuousSMulDiscrete.lean

Statistics

Metric	Count
Definitions ContinuousSMulDiscrete	1
Theorems isOpen_smul_eq, isOpen_stabilizer, of_continuousSMul, continuousSMulDiscrete_iff, continuousSMulDiscrete_iff_isOpen_stabilizer, instContinuousSMulOfDiscreteTopologyOfContinuousSMulDiscrete	6
Total	7

ContinuousSMulDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_smul_eq 📖	—	—	—	—	—
isOpen_stabilizer 📖	—	—	—	—	isOpen_smul_eq
of_continuousSMul 📖	mathematical	—	ContinuousSMulDiscrete	—	continuousSMulDiscrete_iff

(root)

Definitions

Name	Category	Theorems
ContinuousSMulDiscrete 📖	CompData	6 math math: ContinuousSMulDiscrete.of_continuousSMul, instContinuousSMulDiscreteAlgEquivOfIsAlgebraic, continuousSMulDiscrete_iff, continuousSMulDiscrete_integralClosure, instContinuousSMulDiscreteAlgEquivAlgHomOfFinite, continuousSMulDiscrete_iff_isOpen_stabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMulDiscrete_iff 📖	mathematical	—	ContinuousSMulDiscrete	—	ContinuousSMulDiscrete.isOpen_smul_eq
continuousSMulDiscrete_iff_isOpen_stabilizer 📖	mathematical	—	ContinuousSMulDiscrete	—	ContinuousSMulDiscrete.isOpen_smul_eq
instContinuousSMulOfDiscreteTopologyOfContinuousSMulDiscrete 📖	—	—	—	—	continuousSMulDiscrete_iff

---

← Back to Index